Theorem domtr 8929

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 8875	. 2 ⊢ Rel ≼
2		vex 3440	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8883	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3440	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8883	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1956	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6730	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3440	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3440	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7860	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6714	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3556	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8883	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 234	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1933	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 235	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 598	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5677	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   class class class wbr 5089   ∘ ccom 5618  –1-1→wf1 6478   ≼ cdom 8867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-dom 8871

This theorem is referenced by:  endomtr  8934  domentr  8935  cnvct  8956  sdomdomtr  9023  domsdomtr  9025  xpen  9053  unxpdom2  9144  sucxpdom  9145  fidomdm  9218  hartogs  9430  harword  9449  unxpwdom  9475  harcard  9871  infxpenlem  9904  xpct  9907  indcardi  9932  fodomfi2  9951  infpwfien  9953  inffien  9954  djudoml  10076  djuinf  10080  infdju1  10081  djulepw  10084  unctb  10095  infdjuabs  10096  infdju  10098  infdif  10099  infdif2  10100  infxp  10105  infmap2  10108  fictb  10135  cfslb2n  10159  isfin32i  10256  fin1a2lem12  10302  hsmexlem1  10317  dmct  10415  brdom3  10419  brdom5  10420  brdom4  10421  imadomg  10425  fimact  10426  fnct  10428  mptct  10429  iundomg  10432  uniimadom  10435  ondomon  10454  unirnfdomd  10458  alephval2  10463  iunctb  10465  alephexp1  10470  alephreg  10473  cfpwsdom  10475  gchdomtri  10520  canthnum  10540  canthp1lem1  10543  canthp1  10545  pwfseqlem5  10554  pwxpndom2  10556  pwxpndom  10557  pwdjundom  10558  gchdjuidm  10559  gchxpidm  10560  gchpwdom  10561  gchaclem  10569  gchhar  10570  inar1  10666  rankcf  10668  grudomon  10708  grothac  10721  rpnnen  16136  cctop  22921  1stcfb  23360  2ndcredom  23365  2ndc1stc  23366  1stcrestlem  23367  2ndcctbss  23370  2ndcdisj2  23372  2ndcomap  23373  2ndcsep  23374  dis2ndc  23375  hauspwdom  23416  tx1stc  23565  tx2ndc  23566  met2ndci  24437  opnreen  24747  rectbntr0  24748  uniiccdif  25506  dyadmbl  25528  opnmblALT  25531  mbfimaopnlem  25583  abrexdomjm  32487  mptctf  32699  locfinreflem  33853  sigaclci  34145  omsmeas  34336  sibfof  34353  abrexdom  37769  heiborlem3  37852  imadomfi  42094  ttac  43128  idomsubgmo  43285  safesnsupfidom1o  43509  pr2dom  43619  tr3dom  43620  uzct  45159  rn1st  45369  omeiunle  46614  smfaddlem2  46861  smflimlem6  46873  smfmullem4  46891  smfpimbor1lem1  46895