Theorem domtr 8978

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 8924	. 2 ⊢ Rel ≼
2		vex 3451	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8932	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3451	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8932	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1955	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6767	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3451	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3451	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7906	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6751	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3572	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8932	. . . . . 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 5701	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   class class class wbr 5107   ∘ ccom 5642  –1-1→wf1 6508   ≼ cdom 8916

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-dom 8920

This theorem is referenced by:  endomtr  8983  domentr  8984  cnvct  9005  sdomdomtr  9074  domsdomtr  9076  xpen  9104  unxpdom2  9201  sucxpdom  9202  fidomdm  9285  hartogs  9497  harword  9516  unxpwdom  9542  harcard  9931  infxpenlem  9966  xpct  9969  indcardi  9994  fodomfi2  10013  infpwfien  10015  inffien  10016  djudoml  10138  djuinf  10142  infdju1  10143  djulepw  10146  unctb  10157  infdjuabs  10158  infdju  10160  infdif  10161  infdif2  10162  infxp  10167  infmap2  10170  fictb  10197  cfslb2n  10221  isfin32i  10318  fin1a2lem12  10364  hsmexlem1  10379  dmct  10477  brdom3  10481  brdom5  10482  brdom4  10483  imadomg  10487  fimact  10488  fnct  10490  mptct  10491  iundomg  10494  uniimadom  10497  ondomon  10516  unirnfdomd  10520  alephval2  10525  iunctb  10527  alephexp1  10532  alephreg  10535  cfpwsdom  10537  gchdomtri  10582  canthnum  10602  canthp1lem1  10605  canthp1  10607  pwfseqlem5  10616  pwxpndom2  10618  pwxpndom  10619  pwdjundom  10620  gchdjuidm  10621  gchxpidm  10622  gchpwdom  10623  gchaclem  10631  gchhar  10632  inar1  10728  rankcf  10730  grudomon  10770  grothac  10783  rpnnen  16195  cctop  22893  1stcfb  23332  2ndcredom  23337  2ndc1stc  23338  1stcrestlem  23339  2ndcctbss  23342  2ndcdisj2  23344  2ndcomap  23345  2ndcsep  23346  dis2ndc  23347  hauspwdom  23388  tx1stc  23537  tx2ndc  23538  met2ndci  24410  opnreen  24720  rectbntr0  24721  uniiccdif  25479  dyadmbl  25501  opnmblALT  25504  mbfimaopnlem  25556  abrexdomjm  32436  mptctf  32641  locfinreflem  33830  sigaclci  34122  omsmeas  34314  sibfof  34331  abrexdom  37724  heiborlem3  37807  imadomfi  41990  ttac  43025  idomsubgmo  43182  safesnsupfidom1o  43406  pr2dom  43516  tr3dom  43517  uzct  45057  rn1st  45267  omeiunle  46515  smfaddlem2  46762  smflimlem6  46774  smfmullem4  46792  smfpimbor1lem1  46796