Theorem domtr 8955

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 8901	. 2 ⊢ Rel ≼
2		vex 3448	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8909	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3448	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8909	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1955	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6749	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3448	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3448	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7886	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6733	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3569	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8909	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 234	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1932	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 235	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 598	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5694	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   class class class wbr 5102   ∘ ccom 5635  –1-1→wf1 6496   ≼ cdom 8893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-dom 8897

This theorem is referenced by:  endomtr  8960  domentr  8961  cnvct  8982  sdomdomtr  9051  domsdomtr  9053  xpen  9081  unxpdom2  9177  sucxpdom  9178  fidomdm  9261  hartogs  9473  harword  9492  unxpwdom  9518  harcard  9907  infxpenlem  9942  xpct  9945  indcardi  9970  fodomfi2  9989  infpwfien  9991  inffien  9992  djudoml  10114  djuinf  10118  infdju1  10119  djulepw  10122  unctb  10133  infdjuabs  10134  infdju  10136  infdif  10137  infdif2  10138  infxp  10143  infmap2  10146  fictb  10173  cfslb2n  10197  isfin32i  10294  fin1a2lem12  10340  hsmexlem1  10355  dmct  10453  brdom3  10457  brdom5  10458  brdom4  10459  imadomg  10463  fimact  10464  fnct  10466  mptct  10467  iundomg  10470  uniimadom  10473  ondomon  10492  unirnfdomd  10496  alephval2  10501  iunctb  10503  alephexp1  10508  alephreg  10511  cfpwsdom  10513  gchdomtri  10558  canthnum  10578  canthp1lem1  10581  canthp1  10583  pwfseqlem5  10592  pwxpndom2  10594  pwxpndom  10595  pwdjundom  10596  gchdjuidm  10597  gchxpidm  10598  gchpwdom  10599  gchaclem  10607  gchhar  10608  inar1  10704  rankcf  10706  grudomon  10746  grothac  10759  rpnnen  16171  cctop  22926  1stcfb  23365  2ndcredom  23370  2ndc1stc  23371  1stcrestlem  23372  2ndcctbss  23375  2ndcdisj2  23377  2ndcomap  23378  2ndcsep  23379  dis2ndc  23380  hauspwdom  23421  tx1stc  23570  tx2ndc  23571  met2ndci  24443  opnreen  24753  rectbntr0  24754  uniiccdif  25512  dyadmbl  25534  opnmblALT  25537  mbfimaopnlem  25589  abrexdomjm  32486  mptctf  32691  locfinreflem  33823  sigaclci  34115  omsmeas  34307  sibfof  34324  abrexdom  37717  heiborlem3  37800  imadomfi  41983  ttac  43018  idomsubgmo  43175  safesnsupfidom1o  43399  pr2dom  43509  tr3dom  43510  uzct  45050  rn1st  45260  omeiunle  46508  smfaddlem2  46755  smflimlem6  46767  smfmullem4  46785  smfpimbor1lem1  46789