Theorem domtr 8793

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 8739	. 2 ⊢ Rel ≼
2		vex 3436	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8750	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3436	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8750	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1959	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6682	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 459	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3436	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3436	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7777	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6665	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3545	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8750	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 233	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1935	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 234	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 598	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5650	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1782   class class class wbr 5074   ∘ ccom 5593  –1-1→wf1 6430   ≼ cdom 8731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-dom 8735

This theorem is referenced by:  endomtr  8798  domentr  8799  cnvct  8824  ssct  8839  undomOLD  8847  sdomdomtr  8897  domsdomtr  8899  xpen  8927  unxpdom2  9031  sucxpdom  9032  fidomdm  9096  hartogs  9303  harword  9322  unxpwdom  9348  harcard  9736  infxpenlem  9769  xpct  9772  indcardi  9797  fodomfi2  9816  infpwfien  9818  inffien  9819  djudoml  9940  djuinf  9944  infdju1  9945  djulepw  9948  unctb  9961  infdjuabs  9962  infdju  9964  infdif  9965  infdif2  9966  infxp  9971  infmap2  9974  fictb  10001  cfslb2n  10024  isfin32i  10121  fin1a2lem12  10167  hsmexlem1  10182  dmct  10280  brdom3  10284  brdom5  10285  brdom4  10286  imadomg  10290  fimact  10291  fnct  10293  mptct  10294  iundomg  10297  uniimadom  10300  ondomon  10319  unirnfdomd  10323  alephval2  10328  iunctb  10330  alephexp1  10335  alephreg  10338  cfpwsdom  10340  gchdomtri  10385  canthnum  10405  canthp1lem1  10408  canthp1  10410  pwfseqlem5  10419  pwxpndom2  10421  pwxpndom  10422  pwdjundom  10423  gchdjuidm  10424  gchxpidm  10425  gchpwdom  10426  gchaclem  10434  gchhar  10435  inar1  10531  rankcf  10533  grudomon  10573  grothac  10586  rpnnen  15936  cctop  22156  1stcfb  22596  2ndcredom  22601  2ndc1stc  22602  1stcrestlem  22603  2ndcctbss  22606  2ndcdisj2  22608  2ndcomap  22609  2ndcsep  22610  dis2ndc  22611  hauspwdom  22652  tx1stc  22801  tx2ndc  22802  met2ndci  23678  opnreen  23994  rectbntr0  23995  uniiccdif  24742  dyadmbl  24764  opnmblALT  24767  mbfimaopnlem  24819  abrexdomjm  30852  mptctf  31052  locfinreflem  31790  sigaclci  32100  omsmeas  32290  sibfof  32307  abrexdom  35888  heiborlem3  35971  ttac  40858  idomsubgmo  41023  pr2dom  41134  tr3dom  41135  uzct  42611  omeiunle  44055  smfaddlem2  44299  smflimlem6  44311  smfmullem4  44328  smfpimbor1lem1  44332