Theorem domtr 8162

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 8115	. 2 ⊢ Rel ≼
2		vex 3354	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8121	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3354	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8121	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		eeanv 2344	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6251	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 455	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3354	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3354	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7265	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6236	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3451	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8121	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 224	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 2012	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 225	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 585	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5304	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 382  ∃wex 1852   class class class wbr 4786   ∘ ccom 5253  –1-1→wf1 6028   ≼ cdom 8107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-dom 8111

This theorem is referenced by:  endomtr  8167  domentr  8168  cnvct  8186  ssct  8197  undom  8204  sdomdomtr  8249  domsdomtr  8251  xpen  8279  unxpdom2  8324  sucxpdom  8325  fidomdm  8399  hartogs  8605  harword  8626  unxpwdom  8650  harcard  9004  infxpenlem  9036  xpct  9039  indcardi  9064  fodomfi2  9083  infpwfien  9085  inffien  9086  cdadom3  9212  cdainf  9216  infcda1  9217  cdalepw  9220  unctb  9229  infcdaabs  9230  infcda  9232  infdif  9233  infdif2  9234  infxp  9239  infmap2  9242  fictb  9269  cfslb2n  9292  isfin32i  9389  fin1a2lem12  9435  hsmexlem1  9450  dmct  9548  brdom3  9552  brdom5  9553  brdom4  9554  imadomg  9558  fimact  9559  fnct  9561  mptct  9562  iundomg  9565  uniimadom  9568  ondomon  9587  unirnfdomd  9591  alephval2  9596  iunctb  9598  alephexp1  9603  alephreg  9606  cfpwsdom  9608  gchdomtri  9653  canthnum  9673  canthp1lem1  9676  canthp1  9678  pwfseqlem5  9687  pwxpndom2  9689  pwxpndom  9690  pwcdandom  9691  gchcdaidm  9692  gchxpidm  9693  gchpwdom  9694  gchaclem  9702  gchhar  9703  inar1  9799  rankcf  9801  grudomon  9841  grothac  9854  rpnnen  15162  cctop  21031  1stcfb  21469  2ndcredom  21474  2ndc1stc  21475  1stcrestlem  21476  2ndcctbss  21479  2ndcdisj2  21481  2ndcomap  21482  2ndcsep  21483  dis2ndc  21484  hauspwdom  21525  tx1stc  21674  tx2ndc  21675  met2ndci  22547  opnreen  22854  rectbntr0  22855  uniiccdif  23566  dyadmbl  23588  opnmblALT  23591  mbfimaopnlem  23642  abrexdomjm  29683  mptctf  29835  locfinreflem  30247  sigaclci  30535  omsmeas  30725  sibfof  30742  abrexdom  33857  heiborlem3  33944  ttac  38129  idomsubgmo  38302  uzct  39753  omeiunle  41251  smfaddlem2  41492  smflimlem6  41504  smfmullem4  41521  smfpimbor1lem1  41525