Theorem domtr 9016

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 8961	. 2 ⊢ Rel ≼
2		vex 3457	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8969	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3457	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8969	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1988	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6788	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 464	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3457	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3457	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7930	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6770	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3563	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 18	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8969	. . . . . 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 5722	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   class class class wbr 5107   ∘ ccom 5663  –1-1→wf1 6534   ≼ cdom 8953

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 2215  ax-ext 2734  ax-sep 5255  ax-pow 5334  ax-pr 5402  ax-un 7739

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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-dom 8957

This theorem is used by:  endomtr  9021  domentr  9022  cnvct  9044  sdomdomtr  9111  domsdomtr  9113  xpen  9141  unxpdom2  9233  sucxpdom  9234  fidomdm  9304  hartogs  9519  harword  9538  unxpwdom  9564  harcard  9986  infxpenlem  10019  xpct  10022  indcardi  10047  fodomfi2  10066  infpwfien  10068  inffien  10069  djudoml  10190  djuinf  10194  infdju1  10195  djulepw  10198  unctb  10209  infdjuabs  10210  infdju  10212  infdif  10213  infdif2  10214  infxp  10219  infmap2  10222  fictb  10249  cfslb2n  10273  isfin32i  10370  fin1a2lem12  10416  hsmexlem1  10431  dmct  10529  dmctOLD  10530  brdom3  10534  brdom5  10535  brdom4  10536  imadomg  10540  imadomnum  10541  fimact  10542  fimactOLD  10543  fnct  10547  fnctOLD  10548  mptct  10549  iundomg  10552  uniimadom  10555  ondomon  10574  unirnfdomd  10579  alephval2  10584  iunctb  10586  alephexp1  10591  alephreg  10594  cfpwsdom  10596  gchdomtri  10641  canthnum  10661  canthp1lem1  10664  canthp1  10666  pwfseqlem5  10675  pwxpndom2  10677  pwxpndom  10678  pwdjundom  10679  gchdjuidm  10680  gchxpidm  10681  gchpwdom  10682  gchaclem  10690  gchhar  10691  inar1  10787  rankcf  10789  grudomon  10829  grothac  10842  rpnnen  16319  cctop  23232  1stcfb  23671  2ndcredom  23676  2ndc1stc  23677  1stcrestlem  23678  2ndcctbss  23682  2ndcdisj2  23684  2ndcomap  23685  2ndcsep  23686  dis2ndc  23687  hauspwdom  23728  tx1stc  23877  tx2ndc  23878  met2ndci  24749  opnreen  25059  rectbntr0  25060  uniiccdif  25807  dyadmbl  25829  opnmblALT  25832  mbfimaopnlem  25884  abrexdomjm  32968  mptctf  33174  locfinreflem  34337  omsmeas  34821  sibfof  34838  abrexdom  38467  heiborlem3  38550  imadomfi  42855  ttac  43864  idomsubgmo  44021  safesnsupfidom1o  44244  pr2dom  44354  tr3dom  44355  uzct  45884  rn1st  46089  smfaddlem2  47579  smflimlem6  47591  smfmullem4  47609  smfpimbor1lem1  47613