Theorem domtr 8949

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 8894	. 2 ⊢ Rel ≼
2		vex 3434	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8902	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3434	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8902	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1957	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6743	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3434	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3434	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7876	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6727	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3549	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8902	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 234	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1934	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 235	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 599	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5689	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   class class class wbr 5086   ∘ ccom 5630  –1-1→wf1 6491   ≼ cdom 8886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pow 5304  ax-pr 5372  ax-un 7684

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-dom 8890

This theorem is referenced by:  endomtr  8954  domentr  8955  cnvct  8976  sdomdomtr  9043  domsdomtr  9045  xpen  9073  unxpdom2  9165  sucxpdom  9166  fidomdm  9239  hartogs  9454  harword  9473  unxpwdom  9499  harcard  9897  infxpenlem  9930  xpct  9933  indcardi  9958  fodomfi2  9977  infpwfien  9979  inffien  9980  djudoml  10102  djuinf  10106  infdju1  10107  djulepw  10110  unctb  10121  infdjuabs  10122  infdju  10124  infdif  10125  infdif2  10126  infxp  10131  infmap2  10134  fictb  10161  cfslb2n  10185  isfin32i  10282  fin1a2lem12  10328  hsmexlem1  10343  dmct  10441  brdom3  10445  brdom5  10446  brdom4  10447  imadomg  10451  fimact  10452  fnct  10454  mptct  10455  iundomg  10458  uniimadom  10461  ondomon  10480  unirnfdomd  10485  alephval2  10490  iunctb  10492  alephexp1  10497  alephreg  10500  cfpwsdom  10502  gchdomtri  10547  canthnum  10567  canthp1lem1  10570  canthp1  10572  pwfseqlem5  10581  pwxpndom2  10583  pwxpndom  10584  pwdjundom  10585  gchdjuidm  10586  gchxpidm  10587  gchpwdom  10588  gchaclem  10596  gchhar  10597  inar1  10693  rankcf  10695  grudomon  10735  grothac  10748  rpnnen  16189  cctop  22985  1stcfb  23424  2ndcredom  23429  2ndc1stc  23430  1stcrestlem  23431  2ndcctbss  23434  2ndcdisj2  23436  2ndcomap  23437  2ndcsep  23438  dis2ndc  23439  hauspwdom  23480  tx1stc  23629  tx2ndc  23630  met2ndci  24501  opnreen  24811  rectbntr0  24812  uniiccdif  25559  dyadmbl  25581  opnmblALT  25584  mbfimaopnlem  25636  abrexdomjm  32596  mptctf  32808  locfinreflem  34004  sigaclci  34296  omsmeas  34487  sibfof  34504  abrexdom  38071  heiborlem3  38154  imadomfi  42461  ttac  43488  idomsubgmo  43645  safesnsupfidom1o  43868  pr2dom  43978  tr3dom  43979  uzct  45518  rn1st  45726  omeiunle  46969  smfaddlem2  47216  smflimlem6  47228  smfmullem4  47246  smfpimbor1lem1  47250