Theorem domtr 8946

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 8891	. 2 ⊢ Rel ≼
2		vex 3443	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8899	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3443	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8899	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1957	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6740	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3443	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3443	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7872	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6724	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3559	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8899	. . . . . 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 5686	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   class class class wbr 5097   ∘ ccom 5627  –1-1→wf1 6488   ≼ cdom 8883

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 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-dom 8887

This theorem is referenced by:  endomtr  8951  domentr  8952  cnvct  8973  sdomdomtr  9040  domsdomtr  9042  xpen  9070  unxpdom2  9162  sucxpdom  9163  fidomdm  9236  hartogs  9451  harword  9470  unxpwdom  9496  harcard  9892  infxpenlem  9925  xpct  9928  indcardi  9953  fodomfi2  9972  infpwfien  9974  inffien  9975  djudoml  10097  djuinf  10101  infdju1  10102  djulepw  10105  unctb  10116  infdjuabs  10117  infdju  10119  infdif  10120  infdif2  10121  infxp  10126  infmap2  10129  fictb  10156  cfslb2n  10180  isfin32i  10277  fin1a2lem12  10323  hsmexlem1  10338  dmct  10436  brdom3  10440  brdom5  10441  brdom4  10442  imadomg  10446  fimact  10447  fnct  10449  mptct  10450  iundomg  10453  uniimadom  10456  ondomon  10475  unirnfdomd  10480  alephval2  10485  iunctb  10487  alephexp1  10492  alephreg  10495  cfpwsdom  10497  gchdomtri  10542  canthnum  10562  canthp1lem1  10565  canthp1  10567  pwfseqlem5  10576  pwxpndom2  10578  pwxpndom  10579  pwdjundom  10580  gchdjuidm  10581  gchxpidm  10582  gchpwdom  10583  gchaclem  10591  gchhar  10592  inar1  10688  rankcf  10690  grudomon  10730  grothac  10743  rpnnen  16154  cctop  22952  1stcfb  23391  2ndcredom  23396  2ndc1stc  23397  1stcrestlem  23398  2ndcctbss  23401  2ndcdisj2  23403  2ndcomap  23404  2ndcsep  23405  dis2ndc  23406  hauspwdom  23447  tx1stc  23596  tx2ndc  23597  met2ndci  24468  opnreen  24778  rectbntr0  24779  uniiccdif  25537  dyadmbl  25559  opnmblALT  25562  mbfimaopnlem  25614  abrexdomjm  32562  mptctf  32774  locfinreflem  33976  sigaclci  34268  omsmeas  34459  sibfof  34476  abrexdom  37900  heiborlem3  37983  imadomfi  42291  ttac  43315  idomsubgmo  43472  safesnsupfidom1o  43695  pr2dom  43805  tr3dom  43806  uzct  45345  rn1st  45554  omeiunle  46798  smfaddlem2  47045  smflimlem6  47057  smfmullem4  47075  smfpimbor1lem1  47079