Theorem domtr 8945

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 8890	. 2 ⊢ Rel ≼
2		vex 3434	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8898	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3434	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8898	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1957	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6739	. . . . . . . 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 7872	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6723	. . . . . . . 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 8898	. . . . . 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 5685	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   class class class wbr 5086   ∘ ccom 5626  –1-1→wf1 6487   ≼ cdom 8882

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 5231  ax-pow 5300  ax-pr 5368  ax-un 7680

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 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-dom 8886

This theorem is referenced by:  endomtr  8950  domentr  8951  cnvct  8972  sdomdomtr  9039  domsdomtr  9041  xpen  9069  unxpdom2  9161  sucxpdom  9162  fidomdm  9235  hartogs  9450  harword  9469  unxpwdom  9495  harcard  9891  infxpenlem  9924  xpct  9927  indcardi  9952  fodomfi2  9971  infpwfien  9973  inffien  9974  djudoml  10096  djuinf  10100  infdju1  10101  djulepw  10104  unctb  10115  infdjuabs  10116  infdju  10118  infdif  10119  infdif2  10120  infxp  10125  infmap2  10128  fictb  10155  cfslb2n  10179  isfin32i  10276  fin1a2lem12  10322  hsmexlem1  10337  dmct  10435  brdom3  10439  brdom5  10440  brdom4  10441  imadomg  10445  fimact  10446  fnct  10448  mptct  10449  iundomg  10452  uniimadom  10455  ondomon  10474  unirnfdomd  10479  alephval2  10484  iunctb  10486  alephexp1  10491  alephreg  10494  cfpwsdom  10496  gchdomtri  10541  canthnum  10561  canthp1lem1  10564  canthp1  10566  pwfseqlem5  10575  pwxpndom2  10577  pwxpndom  10578  pwdjundom  10579  gchdjuidm  10580  gchxpidm  10581  gchpwdom  10582  gchaclem  10590  gchhar  10591  inar1  10687  rankcf  10689  grudomon  10729  grothac  10742  rpnnen  16153  cctop  22949  1stcfb  23388  2ndcredom  23393  2ndc1stc  23394  1stcrestlem  23395  2ndcctbss  23398  2ndcdisj2  23400  2ndcomap  23401  2ndcsep  23402  dis2ndc  23403  hauspwdom  23444  tx1stc  23593  tx2ndc  23594  met2ndci  24465  opnreen  24775  rectbntr0  24776  uniiccdif  25523  dyadmbl  25545  opnmblALT  25548  mbfimaopnlem  25600  abrexdomjm  32566  mptctf  32778  locfinreflem  33990  sigaclci  34282  omsmeas  34473  sibfof  34490  abrexdom  38042  heiborlem3  38125  imadomfi  42433  ttac  43467  idomsubgmo  43624  safesnsupfidom1o  43847  pr2dom  43957  tr3dom  43958  uzct  45497  rn1st  45705  omeiunle  46949  smfaddlem2  47196  smflimlem6  47208  smfmullem4  47226  smfpimbor1lem1  47230