Theorem domtr 9046

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 8990	. 2 ⊢ Rel ≼
2		vex 3482	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 9000	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3482	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 9000	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1953	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6816	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3482	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3482	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7953	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6800	. . . . . . . 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 9000	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 234	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1930	. . . 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 5752	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1776   class class class wbr 5148   ∘ ccom 5693  –1-1→wf1 6560   ≼ cdom 8982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-dom 8986

This theorem is referenced by:  endomtr  9051  domentr  9052  cnvct  9073  ssctOLD  9091  undomOLD  9099  sdomdomtr  9149  domsdomtr  9151  xpen  9179  unxpdom2  9288  sucxpdom  9289  fidomdm  9372  hartogs  9582  harword  9601  unxpwdom  9627  harcard  10016  infxpenlem  10051  xpct  10054  indcardi  10079  fodomfi2  10098  infpwfien  10100  inffien  10101  djudoml  10223  djuinf  10227  infdju1  10228  djulepw  10231  unctb  10242  infdjuabs  10243  infdju  10245  infdif  10246  infdif2  10247  infxp  10252  infmap2  10255  fictb  10282  cfslb2n  10306  isfin32i  10403  fin1a2lem12  10449  hsmexlem1  10464  dmct  10562  brdom3  10566  brdom5  10567  brdom4  10568  imadomg  10572  fimact  10573  fnct  10575  mptct  10576  iundomg  10579  uniimadom  10582  ondomon  10601  unirnfdomd  10605  alephval2  10610  iunctb  10612  alephexp1  10617  alephreg  10620  cfpwsdom  10622  gchdomtri  10667  canthnum  10687  canthp1lem1  10690  canthp1  10692  pwfseqlem5  10701  pwxpndom2  10703  pwxpndom  10704  pwdjundom  10705  gchdjuidm  10706  gchxpidm  10707  gchpwdom  10708  gchaclem  10716  gchhar  10717  inar1  10813  rankcf  10815  grudomon  10855  grothac  10868  rpnnen  16260  cctop  23029  1stcfb  23469  2ndcredom  23474  2ndc1stc  23475  1stcrestlem  23476  2ndcctbss  23479  2ndcdisj2  23481  2ndcomap  23482  2ndcsep  23483  dis2ndc  23484  hauspwdom  23525  tx1stc  23674  tx2ndc  23675  met2ndci  24551  opnreen  24867  rectbntr0  24868  uniiccdif  25627  dyadmbl  25649  opnmblALT  25652  mbfimaopnlem  25704  abrexdomjm  32535  mptctf  32735  locfinreflem  33801  sigaclci  34113  omsmeas  34305  sibfof  34322  abrexdom  37717  heiborlem3  37800  imadomfi  41984  ttac  43025  idomsubgmo  43182  safesnsupfidom1o  43407  pr2dom  43517  tr3dom  43518  uzct  45003  rn1st  45219  omeiunle  46473  smfaddlem2  46720  smflimlem6  46732  smfmullem4  46750  smfpimbor1lem1  46754