Theorem domtr 9004

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 8949	. 2 ⊢ Rel ≼
2		vex 3465	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8957	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3465	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8957	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1982	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6788	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 463	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3465	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3465	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7927	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6770	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3572	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 18	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8957	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 237	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1959	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 238	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 609	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5725	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1806   class class class wbr 5111   ∘ ccom 5666  –1-1→wf1 6534   ≼ cdom 8941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-pow 5337  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-dom 8945

This theorem is referenced by:  endomtr  9009  domentr  9010  cnvct  9031  sdomdomtr  9098  domsdomtr  9100  xpen  9128  unxpdom2  9220  sucxpdom  9221  fidomdm  9291  hartogs  9506  harword  9525  unxpwdom  9551  harcard  9964  infxpenlem  9997  xpct  10000  indcardi  10025  fodomfi2  10044  infpwfien  10046  inffien  10047  djudoml  10168  djuinf  10172  infdju1  10173  djulepw  10176  unctb  10187  infdjuabs  10188  infdju  10190  infdif  10191  infdif2  10192  infxp  10197  infmap2  10200  fictb  10227  cfslb2n  10252  isfin32i  10349  fin1a2lem12  10395  hsmexlem1  10410  dmct  10508  brdom3  10512  brdom5  10513  brdom4  10514  imadomg  10518  fimact  10519  fnct  10521  mptct  10522  iundomg  10525  uniimadom  10528  ondomon  10547  unirnfdomd  10552  alephval2  10557  iunctb  10559  alephexp1  10564  alephreg  10567  cfpwsdom  10569  gchdomtri  10614  canthnum  10634  canthp1lem1  10637  canthp1  10639  pwfseqlem5  10648  pwxpndom2  10650  pwxpndom  10651  pwdjundom  10652  gchdjuidm  10653  gchxpidm  10654  gchpwdom  10655  gchaclem  10663  gchhar  10664  inar1  10760  rankcf  10762  grudomon  10802  grothac  10815  rpnnen  16283  cctop  23132  1stcfb  23571  2ndcredom  23576  2ndc1stc  23577  1stcrestlem  23578  2ndcctbss  23581  2ndcdisj2  23583  2ndcomap  23584  2ndcsep  23585  dis2ndc  23586  hauspwdom  23627  tx1stc  23776  tx2ndc  23777  met2ndci  24648  opnreen  24958  rectbntr0  24959  uniiccdif  25706  dyadmbl  25728  opnmblALT  25731  mbfimaopnlem  25783  abrexdomjm  32794  mptctf  33002  locfinreflem  34175  sigaclci  34467  omsmeas  34658  sibfof  34675  abrexdom  38304  heiborlem3  38387  imadomfi  42694  ttac  43690  idomsubgmo  43847  safesnsupfidom1o  44070  pr2dom  44180  tr3dom  44181  uzct  45710  rn1st  45915  omeiunle  47158  smfaddlem2  47405  smflimlem6  47417  smfmullem4  47435  smfpimbor1lem1  47439