Theorem domtr 8564

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 8517	. 2 ⊢ Rel ≼
2		vex 3499	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8523	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3499	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8523	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1956	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6587	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 461	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3499	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3499	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7637	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6572	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3609	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8523	. . . . . 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 5617	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1780   class class class wbr 5068   ∘ ccom 5561  –1-1→wf1 6354   ≼ cdom 8509

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 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-dom 8513

This theorem is referenced by:  endomtr  8569  domentr  8570  cnvct  8588  ssct  8600  undom  8607  sdomdomtr  8652  domsdomtr  8654  xpen  8682  unxpdom2  8728  sucxpdom  8729  fidomdm  8803  hartogs  9010  harword  9031  unxpwdom  9055  harcard  9409  infxpenlem  9441  xpct  9444  indcardi  9469  fodomfi2  9488  infpwfien  9490  inffien  9491  djudoml  9612  djuinf  9616  infdju1  9617  djulepw  9620  unctb  9629  infdjuabs  9630  infdju  9632  infdif  9633  infdif2  9634  infxp  9639  infmap2  9642  fictb  9669  cfslb2n  9692  isfin32i  9789  fin1a2lem12  9835  hsmexlem1  9850  dmct  9948  brdom3  9952  brdom5  9953  brdom4  9954  imadomg  9958  fimact  9959  fnct  9961  mptct  9962  iundomg  9965  uniimadom  9968  ondomon  9987  unirnfdomd  9991  alephval2  9996  iunctb  9998  alephexp1  10003  alephreg  10006  cfpwsdom  10008  gchdomtri  10053  canthnum  10073  canthp1lem1  10076  canthp1  10078  pwfseqlem5  10087  pwxpndom2  10089  pwxpndom  10090  pwdjundom  10091  gchdjuidm  10092  gchxpidm  10093  gchpwdom  10094  gchaclem  10102  gchhar  10103  inar1  10199  rankcf  10201  grudomon  10241  grothac  10254  rpnnen  15582  cctop  21616  1stcfb  22055  2ndcredom  22060  2ndc1stc  22061  1stcrestlem  22062  2ndcctbss  22065  2ndcdisj2  22067  2ndcomap  22068  2ndcsep  22069  dis2ndc  22070  hauspwdom  22111  tx1stc  22260  tx2ndc  22261  met2ndci  23134  opnreen  23441  rectbntr0  23442  uniiccdif  24181  dyadmbl  24203  opnmblALT  24206  mbfimaopnlem  24258  abrexdomjm  30269  mptctf  30455  locfinreflem  31106  sigaclci  31393  omsmeas  31583  sibfof  31600  abrexdom  35007  heiborlem3  35093  ttac  39640  idomsubgmo  39805  pr2dom  39900  tr3dom  39901  uzct  41332  omeiunle  42806  smfaddlem2  43047  smflimlem6  43059  smfmullem4  43076  smfpimbor1lem1  43080