Theorem domtr 8748

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 8697	. 2 ⊢ Rel ≼
2		vex 3426	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8705	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3426	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8705	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1960	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6666	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3426	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3426	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7751	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6649	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3535	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8705	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 233	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1936	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 234	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 597	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5641	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1783   class class class wbr 5070   ∘ ccom 5584  –1-1→wf1 6415   ≼ cdom 8689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-dom 8693

This theorem is referenced by:  endomtr  8753  domentr  8754  cnvct  8778  ssct  8793  undom  8800  sdomdomtr  8846  domsdomtr  8848  xpen  8876  unxpdom2  8960  sucxpdom  8961  fidomdm  9026  hartogs  9233  harword  9252  unxpwdom  9278  harcard  9667  infxpenlem  9700  xpct  9703  indcardi  9728  fodomfi2  9747  infpwfien  9749  inffien  9750  djudoml  9871  djuinf  9875  infdju1  9876  djulepw  9879  unctb  9892  infdjuabs  9893  infdju  9895  infdif  9896  infdif2  9897  infxp  9902  infmap2  9905  fictb  9932  cfslb2n  9955  isfin32i  10052  fin1a2lem12  10098  hsmexlem1  10113  dmct  10211  brdom3  10215  brdom5  10216  brdom4  10217  imadomg  10221  fimact  10222  fnct  10224  mptct  10225  iundomg  10228  uniimadom  10231  ondomon  10250  unirnfdomd  10254  alephval2  10259  iunctb  10261  alephexp1  10266  alephreg  10269  cfpwsdom  10271  gchdomtri  10316  canthnum  10336  canthp1lem1  10339  canthp1  10341  pwfseqlem5  10350  pwxpndom2  10352  pwxpndom  10353  pwdjundom  10354  gchdjuidm  10355  gchxpidm  10356  gchpwdom  10357  gchaclem  10365  gchhar  10366  inar1  10462  rankcf  10464  grudomon  10504  grothac  10517  rpnnen  15864  cctop  22064  1stcfb  22504  2ndcredom  22509  2ndc1stc  22510  1stcrestlem  22511  2ndcctbss  22514  2ndcdisj2  22516  2ndcomap  22517  2ndcsep  22518  dis2ndc  22519  hauspwdom  22560  tx1stc  22709  tx2ndc  22710  met2ndci  23584  opnreen  23900  rectbntr0  23901  uniiccdif  24647  dyadmbl  24669  opnmblALT  24672  mbfimaopnlem  24724  abrexdomjm  30753  mptctf  30954  locfinreflem  31692  sigaclci  32000  omsmeas  32190  sibfof  32207  abrexdom  35815  heiborlem3  35898  ttac  40774  idomsubgmo  40939  pr2dom  41032  tr3dom  41033  uzct  42500  omeiunle  43945  smfaddlem2  44186  smflimlem6  44198  smfmullem4  44215  smfpimbor1lem1  44219