Theorem domtr 8562

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 8515	. 2 ⊢ Rel ≼
2		vex 3497	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8521	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3497	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8521	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1956	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6585	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 461	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3497	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3497	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7635	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6570	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3607	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8521	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 236	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1933	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 237	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 599	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5615	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1780   class class class wbr 5066   ∘ ccom 5559  –1-1→wf1 6352   ≼ cdom 8507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-dom 8511

This theorem is referenced by:  endomtr  8567  domentr  8568  cnvct  8586  ssct  8598  undom  8605  sdomdomtr  8650  domsdomtr  8652  xpen  8680  unxpdom2  8726  sucxpdom  8727  fidomdm  8801  hartogs  9008  harword  9029  unxpwdom  9053  harcard  9407  infxpenlem  9439  xpct  9442  indcardi  9467  fodomfi2  9486  infpwfien  9488  inffien  9489  djudoml  9610  djuinf  9614  infdju1  9615  djulepw  9618  unctb  9627  infdjuabs  9628  infdju  9630  infdif  9631  infdif2  9632  infxp  9637  infmap2  9640  fictb  9667  cfslb2n  9690  isfin32i  9787  fin1a2lem12  9833  hsmexlem1  9848  dmct  9946  brdom3  9950  brdom5  9951  brdom4  9952  imadomg  9956  fimact  9957  fnct  9959  mptct  9960  iundomg  9963  uniimadom  9966  ondomon  9985  unirnfdomd  9989  alephval2  9994  iunctb  9996  alephexp1  10001  alephreg  10004  cfpwsdom  10006  gchdomtri  10051  canthnum  10071  canthp1lem1  10074  canthp1  10076  pwfseqlem5  10085  pwxpndom2  10087  pwxpndom  10088  pwdjundom  10089  gchdjuidm  10090  gchxpidm  10091  gchpwdom  10092  gchaclem  10100  gchhar  10101  inar1  10197  rankcf  10199  grudomon  10239  grothac  10252  rpnnen  15580  cctop  21614  1stcfb  22053  2ndcredom  22058  2ndc1stc  22059  1stcrestlem  22060  2ndcctbss  22063  2ndcdisj2  22065  2ndcomap  22066  2ndcsep  22067  dis2ndc  22068  hauspwdom  22109  tx1stc  22258  tx2ndc  22259  met2ndci  23132  opnreen  23439  rectbntr0  23440  uniiccdif  24179  dyadmbl  24201  opnmblALT  24204  mbfimaopnlem  24256  abrexdomjm  30267  mptctf  30453  locfinreflem  31104  sigaclci  31391  omsmeas  31581  sibfof  31598  abrexdom  35020  heiborlem3  35106  ttac  39653  idomsubgmo  39818  pr2dom  39913  tr3dom  39914  uzct  41345  omeiunle  42819  smfaddlem2  43060  smflimlem6  43072  smfmullem4  43089  smfpimbor1lem1  43093