Theorem domtr 8776

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 8722	. 2 ⊢ Rel ≼
2		vex 3435	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8733	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3435	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8733	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1963	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6680	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 459	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3435	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3435	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7771	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6663	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3544	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8733	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 233	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1939	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 234	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 598	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5651	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1786   class class class wbr 5079   ∘ ccom 5594  –1-1→wf1 6429   ≼ cdom 8714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-dom 8718

This theorem is referenced by:  endomtr  8781  domentr  8782  cnvct  8807  ssct  8822  undom  8829  sdomdomtr  8879  domsdomtr  8881  xpen  8909  unxpdom2  9009  sucxpdom  9010  fidomdm  9074  hartogs  9281  harword  9300  unxpwdom  9326  harcard  9737  infxpenlem  9770  xpct  9773  indcardi  9798  fodomfi2  9817  infpwfien  9819  inffien  9820  djudoml  9941  djuinf  9945  infdju1  9946  djulepw  9949  unctb  9962  infdjuabs  9963  infdju  9965  infdif  9966  infdif2  9967  infxp  9972  infmap2  9975  fictb  10002  cfslb2n  10025  isfin32i  10122  fin1a2lem12  10168  hsmexlem1  10183  dmct  10281  brdom3  10285  brdom5  10286  brdom4  10287  imadomg  10291  fimact  10292  fnct  10294  mptct  10295  iundomg  10298  uniimadom  10301  ondomon  10320  unirnfdomd  10324  alephval2  10329  iunctb  10331  alephexp1  10336  alephreg  10339  cfpwsdom  10341  gchdomtri  10386  canthnum  10406  canthp1lem1  10409  canthp1  10411  pwfseqlem5  10420  pwxpndom2  10422  pwxpndom  10423  pwdjundom  10424  gchdjuidm  10425  gchxpidm  10426  gchpwdom  10427  gchaclem  10435  gchhar  10436  inar1  10532  rankcf  10534  grudomon  10574  grothac  10587  rpnnen  15934  cctop  22154  1stcfb  22594  2ndcredom  22599  2ndc1stc  22600  1stcrestlem  22601  2ndcctbss  22604  2ndcdisj2  22606  2ndcomap  22607  2ndcsep  22608  dis2ndc  22609  hauspwdom  22650  tx1stc  22799  tx2ndc  22800  met2ndci  23676  opnreen  23992  rectbntr0  23993  uniiccdif  24740  dyadmbl  24762  opnmblALT  24765  mbfimaopnlem  24817  abrexdomjm  30848  mptctf  31048  locfinreflem  31786  sigaclci  32096  omsmeas  32286  sibfof  32303  abrexdom  35884  heiborlem3  35967  ttac  40855  idomsubgmo  41020  pr2dom  41113  tr3dom  41114  uzct  42581  omeiunle  44026  smfaddlem2  44267  smflimlem6  44279  smfmullem4  44296  smfpimbor1lem1  44300