Theorem domtr 9059

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 9004	. 2 ⊢ Rel ≼
2		vex 3458	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 9012	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥⟶1-1𝑦)
4		vex 3458	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 9012	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦⟶1-1𝑧)
6		exdistrv 1990	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥⟶1-1𝑦 ∧ 𝑓:𝑦⟶1-1𝑧) ↔ (∃𝑔 𝑔:𝑥⟶1-1𝑦 ∧ ∃𝑓 𝑓:𝑦⟶1-1𝑧))
7		f1co 6810	. . . . . . . 8 ⊢ ((𝑓:𝑦⟶1-1𝑧 ∧ 𝑔:𝑥⟶1-1𝑦) → (𝑓 ∘ 𝑔):𝑥⟶1-1𝑧)
8	7	ancoms 464	. . . . . . 7 ⊢ ((𝑔:𝑥⟶1-1𝑦 ∧ 𝑓:𝑦⟶1-1𝑧) → (𝑓 ∘ 𝑔):𝑥⟶1-1𝑧)
9		vex 3458	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3458	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7963	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6792	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥⟶1-1𝑧 ↔ (𝑓 ∘ 𝑔):𝑥⟶1-1𝑧))
13	11, 12	spcev 3564	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥⟶1-1𝑧 → ∃ℎ ℎ:𝑥⟶1-1𝑧)
14	8, 13	syl 18	. . . . . 6 ⊢ ((𝑔:𝑥⟶1-1𝑦 ∧ 𝑓:𝑦⟶1-1𝑧) → ∃ℎ ℎ:𝑥⟶1-1𝑧)
15	4	brdom 9012	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥⟶1-1𝑧)
16	14, 15	sylibr 237	. . . . 5 ⊢ ((𝑔:𝑥⟶1-1𝑦 ∧ 𝑓:𝑦⟶1-1𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1967	. . . 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 5718	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   class class class wbr 5106   ∘ ccom 5659  ⟶1-1wf1 6552   ≼ cdom 8996

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-pr 5395  ax-un 7772

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 2102  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-dom 9000

This theorem is used by:  endomtr  9064  domentr  9065  cnvct  9087  sdomdomtr  9154  domsdomtr  9156  xpen  9184  unxpdom2  9276  sucxpdom  9277  fidomdm  9348  hartogs  9562  harword  9581  unxpwdom  9607  harcard  10083  infxpenlem  10116  xpct  10119  indcardi  10144  fodomfi2  10163  infpwfien  10165  inffien  10166  djudoml  10287  djuinf  10291  infdju1  10292  djulepw  10295  unctb  10306  infdjuabs  10307  infdju  10309  infdif  10310  infdif2  10311  infxp  10316  infmap2  10319  fictb  10346  cfslb2n  10370  isfin32i  10467  fin1a2lem12  10513  hsmexlem1  10528  dmct  10626  dmctOLD  10627  brdom3  10631  brdom5  10632  brdom4  10633  imadomg  10637  imadomnum  10638  fimact  10639  fimactOLD  10640  fnct  10644  fnctOLD  10645  mptct  10646  iundomg  10649  uniimadom  10652  ondomon  10671  unirnfdomd  10676  alephval2  10681  iunctb  10683  alephexp1  10688  alephreg  10691  cfpwsdom  10693  gchdomtri  10738  canthnum  10758  canthp1lem1  10761  canthp1  10763  pwfseqlem5  10772  pwxpndom2  10774  pwxpndom  10775  pwdjundom  10776  gchdjuidm  10777  gchxpidm  10778  gchpwdom  10779  gchaclem  10787  gchhar  10788  inar1  10884  rankcf  10886  grudomon  10926  grothac  10939  rpnnen  16421  cctop  23351  1stcfb  23790  2ndcredom  23795  2ndc1stc  23796  1stcrestlem  23797  2ndcctbss  23801  2ndcdisj2  23803  2ndcomap  23804  2ndcsep  23805  dis2ndc  23806  hauspwdom  23847  tx1stc  23996  tx2ndc  23997  met2ndci  24868  opnreen  25178  rectbntr0  25179  uniiccdif  25926  dyadmbl  25948  opnmblALT  25951  mbfimaopnlem  26003  abrexdomjm  33172  mptctf  33376  locfinreflem  34539  omsmeas  35022  sibfof  35039  jltalephlem  36024  abrexdom  38855  heiborlem3  38938  imadomfi  43243  ttac  44234  idomsubgmo  44385  safesnsupfidom1o  44608  pr2dom  44718  tr3dom  44719  uzct  46283  rn1st  46488  subsaliuncl  47571  smfaddlem2  47977  smflimlem6  47989  smfmullem4  48007  smfpimbor1lem1  48011