Theorem domtr 8943

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 8888	. 2 ⊢ Rel ≼
2		vex 3431	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8896	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3431	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8896	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1957	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6736	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3431	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3431	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7870	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6720	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3546	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8896	. . . . . 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 5683	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   class class class wbr 5074   ∘ ccom 5624  –1-1→wf1 6484   ≼ cdom 8880

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 2184  ax-ext 2707  ax-sep 5220  ax-pow 5296  ax-pr 5364  ax-un 7678

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-dom 8884

This theorem is referenced by:  endomtr  8948  domentr  8949  cnvct  8970  sdomdomtr  9037  domsdomtr  9039  xpen  9067  unxpdom2  9159  sucxpdom  9160  fidomdm  9233  hartogs  9448  harword  9467  unxpwdom  9493  harcard  9891  infxpenlem  9924  xpct  9927  indcardi  9952  fodomfi2  9971  infpwfien  9973  inffien  9974  djudoml  10096  djuinf  10100  infdju1  10101  djulepw  10104  unctb  10115  infdjuabs  10116  infdju  10118  infdif  10119  infdif2  10120  infxp  10125  infmap2  10128  fictb  10155  cfslb2n  10179  isfin32i  10276  fin1a2lem12  10322  hsmexlem1  10337  dmct  10435  brdom3  10439  brdom5  10440  brdom4  10441  imadomg  10445  fimact  10446  fnct  10448  mptct  10449  iundomg  10452  uniimadom  10455  ondomon  10474  unirnfdomd  10479  alephval2  10484  iunctb  10486  alephexp1  10491  alephreg  10494  cfpwsdom  10496  gchdomtri  10541  canthnum  10561  canthp1lem1  10564  canthp1  10566  pwfseqlem5  10575  pwxpndom2  10577  pwxpndom  10578  pwdjundom  10579  gchdjuidm  10580  gchxpidm  10581  gchpwdom  10582  gchaclem  10590  gchhar  10591  inar1  10687  rankcf  10689  grudomon  10729  grothac  10742  rpnnen  16183  cctop  22959  1stcfb  23398  2ndcredom  23403  2ndc1stc  23404  1stcrestlem  23405  2ndcctbss  23408  2ndcdisj2  23410  2ndcomap  23411  2ndcsep  23412  dis2ndc  23413  hauspwdom  23454  tx1stc  23603  tx2ndc  23604  met2ndci  24475  opnreen  24785  rectbntr0  24786  uniiccdif  25533  dyadmbl  25555  opnmblALT  25558  mbfimaopnlem  25610  abrexdomjm  32565  mptctf  32777  locfinreflem  33972  sigaclci  34264  omsmeas  34455  sibfof  34472  abrexdom  38039  heiborlem3  38122  imadomfi  42429  ttac  43452  idomsubgmo  43609  safesnsupfidom1o  43832  pr2dom  43942  tr3dom  43943  uzct  45482  rn1st  45690  omeiunle  46933  smfaddlem2  47180  smflimlem6  47192  smfmullem4  47210  smfpimbor1lem1  47214