Theorem domtr 8990

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 8935	. 2 ⊢ Rel ≼
2		vex 3460	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8943	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3460	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8943	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1977	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6775	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 462	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3460	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3460	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7913	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6757	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3567	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8943	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 236	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1954	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 237	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 607	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5712	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1801   class class class wbr 5102   ∘ ccom 5653  –1-1→wf1 6520   ≼ cdom 8927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-pow 5324  ax-pr 5392  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-id 5544  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-dom 8931

This theorem is referenced by:  endomtr  8995  domentr  8996  cnvct  9017  sdomdomtr  9084  domsdomtr  9086  xpen  9114  unxpdom2  9206  sucxpdom  9207  fidomdm  9279  hartogs  9494  harword  9513  unxpwdom  9539  harcard  9938  infxpenlem  9971  xpct  9974  indcardi  9999  fodomfi2  10018  infpwfien  10020  inffien  10021  djudoml  10143  djuinf  10147  infdju1  10148  djulepw  10151  unctb  10162  infdjuabs  10163  infdju  10165  infdif  10166  infdif2  10167  infxp  10172  infmap2  10175  fictb  10202  cfslb2n  10227  isfin32i  10324  fin1a2lem12  10370  hsmexlem1  10385  dmct  10483  brdom3  10487  brdom5  10488  brdom4  10489  imadomg  10493  fimact  10494  fnct  10496  mptct  10497  iundomg  10500  uniimadom  10503  ondomon  10522  unirnfdomd  10527  alephval2  10532  iunctb  10534  alephexp1  10539  alephreg  10542  cfpwsdom  10544  gchdomtri  10589  canthnum  10609  canthp1lem1  10612  canthp1  10614  pwfseqlem5  10623  pwxpndom2  10625  pwxpndom  10626  pwdjundom  10627  gchdjuidm  10628  gchxpidm  10629  gchpwdom  10630  gchaclem  10638  gchhar  10639  inar1  10735  rankcf  10737  grudomon  10777  grothac  10790  rpnnen  16261  cctop  23068  1stcfb  23507  2ndcredom  23512  2ndc1stc  23513  1stcrestlem  23514  2ndcctbss  23517  2ndcdisj2  23519  2ndcomap  23520  2ndcsep  23521  dis2ndc  23522  hauspwdom  23563  tx1stc  23712  tx2ndc  23713  met2ndci  24584  opnreen  24894  rectbntr0  24895  uniiccdif  25642  dyadmbl  25664  opnmblALT  25667  mbfimaopnlem  25719  abrexdomjm  32708  mptctf  32920  locfinreflem  34139  sigaclci  34431  omsmeas  34622  sibfof  34639  abrexdom  38234  heiborlem3  38317  imadomfi  42624  ttac  43618  idomsubgmo  43775  safesnsupfidom1o  43998  pr2dom  44108  tr3dom  44109  uzct  45648  rn1st  45853  omeiunle  47096  smfaddlem2  47343  smflimlem6  47355  smfmullem4  47373  smfpimbor1lem1  47377