Theorem domtr 9028

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 8970	. 2 ⊢ Rel ≼
2		vex 3475	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8981	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3475	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8981	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1952	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6805	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3475	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3475	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7938	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6788	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3593	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8981	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 233	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1928	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 234	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 597	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5741	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1774   class class class wbr 5148   ∘ ccom 5682  –1-1→wf1 6545   ≼ cdom 8962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-opab 5211  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-dom 8966

This theorem is referenced by:  endomtr  9033  domentr  9034  cnvct  9059  ssctOLD  9077  undomOLD  9085  sdomdomtr  9135  domsdomtr  9137  xpen  9165  unxpdom2  9279  sucxpdom  9280  fidomdm  9354  hartogs  9568  harword  9587  unxpwdom  9613  harcard  10002  infxpenlem  10037  xpct  10040  indcardi  10065  fodomfi2  10084  infpwfien  10086  inffien  10087  djudoml  10208  djuinf  10212  infdju1  10213  djulepw  10216  unctb  10229  infdjuabs  10230  infdju  10232  infdif  10233  infdif2  10234  infxp  10239  infmap2  10242  fictb  10269  cfslb2n  10292  isfin32i  10389  fin1a2lem12  10435  hsmexlem1  10450  dmct  10548  brdom3  10552  brdom5  10553  brdom4  10554  imadomg  10558  fimact  10559  fnct  10561  mptct  10562  iundomg  10565  uniimadom  10568  ondomon  10587  unirnfdomd  10591  alephval2  10596  iunctb  10598  alephexp1  10603  alephreg  10606  cfpwsdom  10608  gchdomtri  10653  canthnum  10673  canthp1lem1  10676  canthp1  10678  pwfseqlem5  10687  pwxpndom2  10689  pwxpndom  10690  pwdjundom  10691  gchdjuidm  10692  gchxpidm  10693  gchpwdom  10694  gchaclem  10702  gchhar  10703  inar1  10799  rankcf  10801  grudomon  10841  grothac  10854  rpnnen  16204  cctop  22922  1stcfb  23362  2ndcredom  23367  2ndc1stc  23368  1stcrestlem  23369  2ndcctbss  23372  2ndcdisj2  23374  2ndcomap  23375  2ndcsep  23376  dis2ndc  23377  hauspwdom  23418  tx1stc  23567  tx2ndc  23568  met2ndci  24444  opnreen  24760  rectbntr0  24761  uniiccdif  25520  dyadmbl  25542  opnmblALT  25545  mbfimaopnlem  25597  abrexdomjm  32315  mptctf  32512  locfinreflem  33441  sigaclci  33751  omsmeas  33943  sibfof  33960  abrexdom  37203  heiborlem3  37286  imadomfi  41473  ttac  42457  idomsubgmo  42621  safesnsupfidom1o  42847  pr2dom  42957  tr3dom  42958  uzct  44427  rn1st  44650  omeiunle  45905  smfaddlem2  46152  smflimlem6  46164  smfmullem4  46182  smfpimbor1lem1  46186