Theorem domtr 9034

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 8979	. 2 ⊢ Rel ≼
2		vex 3454	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8987	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3454	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8987	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1987	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6791	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 464	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3454	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3454	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7942	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6773	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3560	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 18	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8987	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 237	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1964	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 238	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 610	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5713	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1811   class class class wbr 5102   ∘ ccom 5654  –1-1→wf1 6535   ≼ cdom 8971

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-dom 8975

This theorem is used by:  endomtr  9039  domentr  9040  cnvct  9062  sdomdomtr  9129  domsdomtr  9131  xpen  9159  unxpdom2  9251  sucxpdom  9252  fidomdm  9323  hartogs  9538  harword  9557  unxpwdom  9583  harcard  10059  infxpenlem  10092  xpct  10095  indcardi  10120  fodomfi2  10139  infpwfien  10141  inffien  10142  djudoml  10263  djuinf  10267  infdju1  10268  djulepw  10271  unctb  10282  infdjuabs  10283  infdju  10285  infdif  10286  infdif2  10287  infxp  10292  infmap2  10295  fictb  10322  cfslb2n  10346  isfin32i  10443  fin1a2lem12  10489  hsmexlem1  10504  dmct  10602  dmctOLD  10603  brdom3  10607  brdom5  10608  brdom4  10609  imadomg  10613  imadomnum  10614  fimact  10615  fimactOLD  10616  fnct  10620  fnctOLD  10621  mptct  10622  iundomg  10625  uniimadom  10628  ondomon  10647  unirnfdomd  10652  alephval2  10657  iunctb  10659  alephexp1  10664  alephreg  10667  cfpwsdom  10669  gchdomtri  10714  canthnum  10734  canthp1lem1  10737  canthp1  10739  pwfseqlem5  10748  pwxpndom2  10750  pwxpndom  10751  pwdjundom  10752  gchdjuidm  10753  gchxpidm  10754  gchpwdom  10755  gchaclem  10763  gchhar  10764  inar1  10860  rankcf  10862  grudomon  10902  grothac  10915  rpnnen  16395  cctop  23324  1stcfb  23763  2ndcredom  23768  2ndc1stc  23769  1stcrestlem  23770  2ndcctbss  23774  2ndcdisj2  23776  2ndcomap  23777  2ndcsep  23778  dis2ndc  23779  hauspwdom  23820  tx1stc  23969  tx2ndc  23970  met2ndci  24841  opnreen  25151  rectbntr0  25152  uniiccdif  25899  dyadmbl  25921  opnmblALT  25924  mbfimaopnlem  25976  abrexdomjm  33103  mptctf  33308  locfinreflem  34472  omsmeas  34955  sibfof  34972  abrexdom  38665  heiborlem3  38748  imadomfi  43053  ttac  44043  idomsubgmo  44195  safesnsupfidom1o  44418  pr2dom  44528  tr3dom  44529  uzct  46080  rn1st  46285  subsaliuncl  47368  smfaddlem2  47774  smflimlem6  47786  smfmullem4  47804  smfpimbor1lem1  47808