Theorem domtr 9047

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 8991	. 2 ⊢ Rel ≼
2		vex 3484	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 9001	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3484	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 9001	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1955	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6815	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3484	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3484	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7952	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6799	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3606	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 9001	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 234	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1932	. . . 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 5748	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   class class class wbr 5143   ∘ ccom 5689  –1-1→wf1 6558   ≼ cdom 8983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-dom 8987

This theorem is referenced by:  endomtr  9052  domentr  9053  cnvct  9074  ssctOLD  9092  undomOLD  9100  sdomdomtr  9150  domsdomtr  9152  xpen  9180  unxpdom2  9290  sucxpdom  9291  fidomdm  9374  hartogs  9584  harword  9603  unxpwdom  9629  harcard  10018  infxpenlem  10053  xpct  10056  indcardi  10081  fodomfi2  10100  infpwfien  10102  inffien  10103  djudoml  10225  djuinf  10229  infdju1  10230  djulepw  10233  unctb  10244  infdjuabs  10245  infdju  10247  infdif  10248  infdif2  10249  infxp  10254  infmap2  10257  fictb  10284  cfslb2n  10308  isfin32i  10405  fin1a2lem12  10451  hsmexlem1  10466  dmct  10564  brdom3  10568  brdom5  10569  brdom4  10570  imadomg  10574  fimact  10575  fnct  10577  mptct  10578  iundomg  10581  uniimadom  10584  ondomon  10603  unirnfdomd  10607  alephval2  10612  iunctb  10614  alephexp1  10619  alephreg  10622  cfpwsdom  10624  gchdomtri  10669  canthnum  10689  canthp1lem1  10692  canthp1  10694  pwfseqlem5  10703  pwxpndom2  10705  pwxpndom  10706  pwdjundom  10707  gchdjuidm  10708  gchxpidm  10709  gchpwdom  10710  gchaclem  10718  gchhar  10719  inar1  10815  rankcf  10817  grudomon  10857  grothac  10870  rpnnen  16263  cctop  23013  1stcfb  23453  2ndcredom  23458  2ndc1stc  23459  1stcrestlem  23460  2ndcctbss  23463  2ndcdisj2  23465  2ndcomap  23466  2ndcsep  23467  dis2ndc  23468  hauspwdom  23509  tx1stc  23658  tx2ndc  23659  met2ndci  24535  opnreen  24853  rectbntr0  24854  uniiccdif  25613  dyadmbl  25635  opnmblALT  25638  mbfimaopnlem  25690  abrexdomjm  32526  mptctf  32729  locfinreflem  33839  sigaclci  34133  omsmeas  34325  sibfof  34342  abrexdom  37737  heiborlem3  37820  imadomfi  42003  ttac  43048  idomsubgmo  43205  safesnsupfidom1o  43430  pr2dom  43540  tr3dom  43541  uzct  45068  rn1st  45280  omeiunle  46532  smfaddlem2  46779  smflimlem6  46791  smfmullem4  46809  smfpimbor1lem1  46813