Theorem domtr 8932

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 8878	. 2 ⊢ Rel ≼
2		vex 3440	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8886	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3440	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8886	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1955	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6731	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3440	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3440	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7863	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6715	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3561	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8886	. . . . . 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 5682	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   class class class wbr 5092   ∘ ccom 5623  –1-1→wf1 6479   ≼ cdom 8870

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 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-dom 8874

This theorem is referenced by:  endomtr  8937  domentr  8938  cnvct  8959  sdomdomtr  9027  domsdomtr  9029  xpen  9057  unxpdom2  9149  sucxpdom  9150  fidomdm  9224  hartogs  9436  harword  9455  unxpwdom  9481  harcard  9874  infxpenlem  9907  xpct  9910  indcardi  9935  fodomfi2  9954  infpwfien  9956  inffien  9957  djudoml  10079  djuinf  10083  infdju1  10084  djulepw  10087  unctb  10098  infdjuabs  10099  infdju  10101  infdif  10102  infdif2  10103  infxp  10108  infmap2  10111  fictb  10138  cfslb2n  10162  isfin32i  10259  fin1a2lem12  10305  hsmexlem1  10320  dmct  10418  brdom3  10422  brdom5  10423  brdom4  10424  imadomg  10428  fimact  10429  fnct  10431  mptct  10432  iundomg  10435  uniimadom  10438  ondomon  10457  unirnfdomd  10461  alephval2  10466  iunctb  10468  alephexp1  10473  alephreg  10476  cfpwsdom  10478  gchdomtri  10523  canthnum  10543  canthp1lem1  10546  canthp1  10548  pwfseqlem5  10557  pwxpndom2  10559  pwxpndom  10560  pwdjundom  10561  gchdjuidm  10562  gchxpidm  10563  gchpwdom  10564  gchaclem  10572  gchhar  10573  inar1  10669  rankcf  10671  grudomon  10711  grothac  10724  rpnnen  16136  cctop  22891  1stcfb  23330  2ndcredom  23335  2ndc1stc  23336  1stcrestlem  23337  2ndcctbss  23340  2ndcdisj2  23342  2ndcomap  23343  2ndcsep  23344  dis2ndc  23345  hauspwdom  23386  tx1stc  23535  tx2ndc  23536  met2ndci  24408  opnreen  24718  rectbntr0  24719  uniiccdif  25477  dyadmbl  25499  opnmblALT  25502  mbfimaopnlem  25554  abrexdomjm  32456  mptctf  32668  locfinreflem  33823  sigaclci  34115  omsmeas  34307  sibfof  34324  abrexdom  37730  heiborlem3  37813  imadomfi  41995  ttac  43029  idomsubgmo  43186  safesnsupfidom1o  43410  pr2dom  43520  tr3dom  43521  uzct  45061  rn1st  45271  omeiunle  46518  smfaddlem2  46765  smflimlem6  46777  smfmullem4  46795  smfpimbor1lem1  46799