Theorem domtr 9013

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 8958	. 2 ⊢ Rel ≼
2		vex 3454	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8966	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3454	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8966	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1988	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6780	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 464	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3454	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3454	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7926	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6762	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3560	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 18	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8966	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 237	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1965	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 238	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 610	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5711	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   class class class wbr 5103   ∘ ccom 5652  –1-1→wf1 6525   ≼ cdom 8950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-dom 8954

This theorem is used by:  endomtr  9018  domentr  9019  cnvct  9041  sdomdomtr  9108  domsdomtr  9110  xpen  9138  unxpdom2  9230  sucxpdom  9231  fidomdm  9301  hartogs  9516  harword  9535  unxpwdom  9561  harcard  10016  infxpenlem  10049  xpct  10052  indcardi  10077  fodomfi2  10096  infpwfien  10098  inffien  10099  djudoml  10220  djuinf  10224  infdju1  10225  djulepw  10228  unctb  10239  infdjuabs  10240  infdju  10242  infdif  10243  infdif2  10244  infxp  10249  infmap2  10252  fictb  10279  cfslb2n  10303  isfin32i  10400  fin1a2lem12  10446  hsmexlem1  10461  dmct  10559  dmctOLD  10560  brdom3  10564  brdom5  10565  brdom4  10566  imadomg  10570  imadomnum  10571  fimact  10572  fimactOLD  10573  fnct  10577  fnctOLD  10578  mptct  10579  iundomg  10582  uniimadom  10585  ondomon  10604  unirnfdomd  10609  alephval2  10614  iunctb  10616  alephexp1  10621  alephreg  10624  cfpwsdom  10626  gchdomtri  10671  canthnum  10691  canthp1lem1  10694  canthp1  10696  pwfseqlem5  10705  pwxpndom2  10707  pwxpndom  10708  pwdjundom  10709  gchdjuidm  10710  gchxpidm  10711  gchpwdom  10712  gchaclem  10720  gchhar  10721  inar1  10817  rankcf  10819  grudomon  10859  grothac  10872  rpnnen  16348  cctop  23271  1stcfb  23710  2ndcredom  23715  2ndc1stc  23716  1stcrestlem  23717  2ndcctbss  23721  2ndcdisj2  23723  2ndcomap  23724  2ndcsep  23725  dis2ndc  23726  hauspwdom  23767  tx1stc  23916  tx2ndc  23917  met2ndci  24788  opnreen  25098  rectbntr0  25099  uniiccdif  25846  dyadmbl  25868  opnmblALT  25871  mbfimaopnlem  25923  abrexdomjm  33022  mptctf  33227  locfinreflem  34391  omsmeas  34875  sibfof  34892  abrexdom  38578  heiborlem3  38661  imadomfi  42966  ttac  43975  idomsubgmo  44132  safesnsupfidom1o  44355  pr2dom  44465  tr3dom  44466  uzct  45995  rn1st  46200  subsaliuncl  47284  smfaddlem2  47690  smflimlem6  47702  smfmullem4  47720  smfpimbor1lem1  47724