Theorem domtr 9002

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 8947	. 2 ⊢ Rel ≼
2		vex 3458	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8955	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3458	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8955	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1984	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6787	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 463	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3458	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3458	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7925	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6769	. . . . . . . 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 8955	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 237	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1961	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 238	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 609	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5723	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400  ∃wex 1808   class class class wbr 5108   ∘ ccom 5664  –1-1→wf1 6533   ≼ cdom 8939

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-pow 5335  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-dom 8943

This theorem is used by:  endomtr  9007  domentr  9008  cnvct  9029  sdomdomtr  9096  domsdomtr  9098  xpen  9126  unxpdom2  9218  sucxpdom  9219  fidomdm  9289  hartogs  9504  harword  9523  unxpwdom  9549  harcard  9971  infxpenlem  10004  xpct  10007  indcardi  10032  fodomfi2  10051  infpwfien  10053  inffien  10054  djudoml  10175  djuinf  10179  infdju1  10180  djulepw  10183  unctb  10194  infdjuabs  10195  infdju  10197  infdif  10198  infdif2  10199  infxp  10204  infmap2  10207  fictb  10234  cfslb2n  10258  isfin32i  10355  fin1a2lem12  10401  hsmexlem1  10416  dmct  10514  brdom3  10518  brdom5  10519  brdom4  10520  imadomg  10524  fimact  10525  fnct  10527  mptct  10528  iundomg  10531  uniimadom  10534  ondomon  10553  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  16289  cctop  23174  1stcfb  23613  2ndcredom  23618  2ndc1stc  23619  1stcrestlem  23620  2ndcctbss  23623  2ndcdisj2  23625  2ndcomap  23626  2ndcsep  23627  dis2ndc  23628  hauspwdom  23669  tx1stc  23818  tx2ndc  23819  met2ndci  24690  opnreen  25000  rectbntr0  25001  uniiccdif  25748  dyadmbl  25770  opnmblALT  25773  mbfimaopnlem  25825  abrexdomjm  32864  mptctf  33072  locfinreflem  34239  sigaclci  34531  omsmeas  34722  sibfof  34739  abrexdom  38409  heiborlem3  38492  imadomfi  42797  ttac  43791  idomsubgmo  43948  safesnsupfidom1o  44171  pr2dom  44281  tr3dom  44282  uzct  45811  rn1st  46016  omeiunle  47259  smfaddlem2  47506  smflimlem6  47518  smfmullem4  47536  smfpimbor1lem1  47540