Theorem domtr 8009

Description: Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94. (Contributed by NM, 4-Jun-1998.) (Revised by Mario Carneiro, 15-Nov-2014.)

Assertion

Ref	Expression
domtr	⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Proof of Theorem domtr

Dummy variables 𝑥 𝑦 𝑧 𝑓 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reldom 7961	. 2 ⊢ Rel ≼
2		vex 3203	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 7967	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3203	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 7967	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		eeanv 2182	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6110	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 469	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3203	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3203	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7118	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6096	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3300	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 7967	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 224	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1860	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 225	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 496	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5164	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 384  ∃wex 1704   class class class wbr 4653   ∘ ccom 5118  –1-1→wf1 5885   ≼ cdom 7953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-dom 7957

This theorem is referenced by:  endomtr  8014  domentr  8015  cnvct  8033  ssct  8041  undom  8048  sdomdomtr  8093  domsdomtr  8095  xpen  8123  unxpdom2  8168  sucxpdom  8169  fidomdm  8243  hartogs  8449  harword  8470  unxpwdom  8494  harcard  8804  infxpenlem  8836  xpct  8839  indcardi  8864  fodomfi2  8883  infpwfien  8885  inffien  8886  cdadom3  9010  cdainf  9014  infcda1  9015  cdalepw  9018  unctb  9027  infcdaabs  9028  infcda  9030  infdif  9031  infdif2  9032  infxp  9037  infmap2  9040  fictb  9067  cfslb2n  9090  isfin32i  9187  fin1a2lem12  9233  hsmexlem1  9248  dmct  9346  brdom3  9350  brdom5  9351  brdom4  9352  imadomg  9356  fimact  9357  fnct  9359  mptct  9360  iundomg  9363  uniimadom  9366  ondomon  9385  unirnfdomd  9389  alephval2  9394  iunctb  9396  alephexp1  9401  alephreg  9404  cfpwsdom  9406  gchdomtri  9451  canthnum  9471  canthp1lem1  9474  canthp1  9476  pwfseqlem5  9485  pwxpndom2  9487  pwxpndom  9488  pwcdandom  9489  gchcdaidm  9490  gchxpidm  9491  gchpwdom  9492  gchaclem  9500  gchhar  9501  inar1  9597  rankcf  9599  grudomon  9639  grothac  9652  rpnnen  14956  cctop  20810  1stcfb  21248  2ndcredom  21253  2ndc1stc  21254  1stcrestlem  21255  2ndcctbss  21258  2ndcdisj2  21260  2ndcomap  21261  2ndcsep  21262  dis2ndc  21263  hauspwdom  21304  tx1stc  21453  tx2ndc  21454  met2ndci  22327  opnreen  22634  rectbntr0  22635  uniiccdif  23346  dyadmbl  23368  opnmblALT  23371  mbfimaopnlem  23422  abrexdomjm  29345  mptctf  29495  locfinreflem  29907  sigaclci  30195  omsmeas  30385  sibfof  30402  abrexdom  33525  heiborlem3  33612  ttac  37603  idomsubgmo  37776  uzct  39232  omeiunle  40731  smfaddlem2  40972  smflimlem6  40984  smfmullem4  41001  smfpimbor1lem1  41005