Theorem domtr 8999

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 8941	. 2 ⊢ Rel ≼
2		vex 3478	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8952	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3478	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8952	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1959	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6796	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 459	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3478	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3478	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7917	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6779	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3596	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8952	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 233	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1935	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 234	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 598	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5737	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1781   class class class wbr 5147   ∘ ccom 5679  –1-1→wf1 6537   ≼ cdom 8933

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-dom 8937

This theorem is referenced by:  endomtr  9004  domentr  9005  cnvct  9030  ssctOLD  9048  undomOLD  9056  sdomdomtr  9106  domsdomtr  9108  xpen  9136  unxpdom2  9250  sucxpdom  9251  fidomdm  9325  hartogs  9535  harword  9554  unxpwdom  9580  harcard  9969  infxpenlem  10004  xpct  10007  indcardi  10032  fodomfi2  10051  infpwfien  10053  inffien  10054  djudoml  10175  djuinf  10179  infdju1  10180  djulepw  10183  unctb  10196  infdjuabs  10197  infdju  10199  infdif  10200  infdif2  10201  infxp  10206  infmap2  10209  fictb  10236  cfslb2n  10259  isfin32i  10356  fin1a2lem12  10402  hsmexlem1  10417  dmct  10515  brdom3  10519  brdom5  10520  brdom4  10521  imadomg  10525  fimact  10526  fnct  10528  mptct  10529  iundomg  10532  uniimadom  10535  ondomon  10554  unirnfdomd  10558  alephval2  10563  iunctb  10565  alephexp1  10570  alephreg  10573  cfpwsdom  10575  gchdomtri  10620  canthnum  10640  canthp1lem1  10643  canthp1  10645  pwfseqlem5  10654  pwxpndom2  10656  pwxpndom  10657  pwdjundom  10658  gchdjuidm  10659  gchxpidm  10660  gchpwdom  10661  gchaclem  10669  gchhar  10670  inar1  10766  rankcf  10768  grudomon  10808  grothac  10821  rpnnen  16166  cctop  22500  1stcfb  22940  2ndcredom  22945  2ndc1stc  22946  1stcrestlem  22947  2ndcctbss  22950  2ndcdisj2  22952  2ndcomap  22953  2ndcsep  22954  dis2ndc  22955  hauspwdom  22996  tx1stc  23145  tx2ndc  23146  met2ndci  24022  opnreen  24338  rectbntr0  24339  uniiccdif  25086  dyadmbl  25108  opnmblALT  25111  mbfimaopnlem  25163  abrexdomjm  31731  mptctf  31929  locfinreflem  32808  sigaclci  33118  omsmeas  33310  sibfof  33327  abrexdom  36586  heiborlem3  36669  ttac  41760  idomsubgmo  41925  safesnsupfidom1o  42153  pr2dom  42263  tr3dom  42264  uzct  43735  rn1st  43964  omeiunle  45219  smfaddlem2  45466  smflimlem6  45478  smfmullem4  45496  smfpimbor1lem1  45500