Theorem domtr 8958

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 8903	. 2 ⊢ Rel ≼
2		vex 3446	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8911	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3446	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8911	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1957	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6751	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3446	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3446	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7884	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6735	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3562	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8911	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 234	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1934	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 235	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 599	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5697	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   class class class wbr 5100   ∘ ccom 5638  –1-1→wf1 6499   ≼ cdom 8895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-pow 5314  ax-pr 5381  ax-un 7692

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-dom 8899

This theorem is referenced by:  endomtr  8963  domentr  8964  cnvct  8985  sdomdomtr  9052  domsdomtr  9054  xpen  9082  unxpdom2  9174  sucxpdom  9175  fidomdm  9248  hartogs  9463  harword  9482  unxpwdom  9508  harcard  9904  infxpenlem  9937  xpct  9940  indcardi  9965  fodomfi2  9984  infpwfien  9986  inffien  9987  djudoml  10109  djuinf  10113  infdju1  10114  djulepw  10117  unctb  10128  infdjuabs  10129  infdju  10131  infdif  10132  infdif2  10133  infxp  10138  infmap2  10141  fictb  10168  cfslb2n  10192  isfin32i  10289  fin1a2lem12  10335  hsmexlem1  10350  dmct  10448  brdom3  10452  brdom5  10453  brdom4  10454  imadomg  10458  fimact  10459  fnct  10461  mptct  10462  iundomg  10465  uniimadom  10468  ondomon  10487  unirnfdomd  10492  alephval2  10497  iunctb  10499  alephexp1  10504  alephreg  10507  cfpwsdom  10509  gchdomtri  10554  canthnum  10574  canthp1lem1  10577  canthp1  10579  pwfseqlem5  10588  pwxpndom2  10590  pwxpndom  10591  pwdjundom  10592  gchdjuidm  10593  gchxpidm  10594  gchpwdom  10595  gchaclem  10603  gchhar  10604  inar1  10700  rankcf  10702  grudomon  10742  grothac  10755  rpnnen  16166  cctop  22967  1stcfb  23406  2ndcredom  23411  2ndc1stc  23412  1stcrestlem  23413  2ndcctbss  23416  2ndcdisj2  23418  2ndcomap  23419  2ndcsep  23420  dis2ndc  23421  hauspwdom  23462  tx1stc  23611  tx2ndc  23612  met2ndci  24483  opnreen  24793  rectbntr0  24794  uniiccdif  25552  dyadmbl  25574  opnmblALT  25577  mbfimaopnlem  25629  abrexdomjm  32600  mptctf  32812  locfinreflem  34024  sigaclci  34316  omsmeas  34507  sibfof  34524  abrexdom  38010  heiborlem3  38093  imadomfi  42401  ttac  43422  idomsubgmo  43579  safesnsupfidom1o  43802  pr2dom  43912  tr3dom  43913  uzct  45452  rn1st  45660  omeiunle  46904  smfaddlem2  47151  smflimlem6  47163  smfmullem4  47181  smfpimbor1lem1  47185