Theorem domtr 9026

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 8970	. 2 ⊢ Rel ≼
2		vex 3468	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8980	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3468	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8980	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1955	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6790	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3468	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3468	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7931	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6774	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3590	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8980	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 234	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1932	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 235	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 598	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5722	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   class class class wbr 5124   ∘ ccom 5663  –1-1→wf1 6533   ≼ cdom 8962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-dom 8966

This theorem is referenced by:  endomtr  9031  domentr  9032  cnvct  9053  ssctOLD  9071  undomOLD  9079  sdomdomtr  9129  domsdomtr  9131  xpen  9159  unxpdom2  9267  sucxpdom  9268  fidomdm  9351  hartogs  9563  harword  9582  unxpwdom  9608  harcard  9997  infxpenlem  10032  xpct  10035  indcardi  10060  fodomfi2  10079  infpwfien  10081  inffien  10082  djudoml  10204  djuinf  10208  infdju1  10209  djulepw  10212  unctb  10223  infdjuabs  10224  infdju  10226  infdif  10227  infdif2  10228  infxp  10233  infmap2  10236  fictb  10263  cfslb2n  10287  isfin32i  10384  fin1a2lem12  10430  hsmexlem1  10445  dmct  10543  brdom3  10547  brdom5  10548  brdom4  10549  imadomg  10553  fimact  10554  fnct  10556  mptct  10557  iundomg  10560  uniimadom  10563  ondomon  10582  unirnfdomd  10586  alephval2  10591  iunctb  10593  alephexp1  10598  alephreg  10601  cfpwsdom  10603  gchdomtri  10648  canthnum  10668  canthp1lem1  10671  canthp1  10673  pwfseqlem5  10682  pwxpndom2  10684  pwxpndom  10685  pwdjundom  10686  gchdjuidm  10687  gchxpidm  10688  gchpwdom  10689  gchaclem  10697  gchhar  10698  inar1  10794  rankcf  10796  grudomon  10836  grothac  10849  rpnnen  16250  cctop  22949  1stcfb  23388  2ndcredom  23393  2ndc1stc  23394  1stcrestlem  23395  2ndcctbss  23398  2ndcdisj2  23400  2ndcomap  23401  2ndcsep  23402  dis2ndc  23403  hauspwdom  23444  tx1stc  23593  tx2ndc  23594  met2ndci  24466  opnreen  24776  rectbntr0  24777  uniiccdif  25536  dyadmbl  25558  opnmblALT  25561  mbfimaopnlem  25613  abrexdomjm  32493  mptctf  32700  locfinreflem  33876  sigaclci  34168  omsmeas  34360  sibfof  34377  abrexdom  37759  heiborlem3  37842  imadomfi  42020  ttac  43035  idomsubgmo  43192  safesnsupfidom1o  43416  pr2dom  43526  tr3dom  43527  uzct  45067  rn1st  45277  omeiunle  46526  smfaddlem2  46773  smflimlem6  46785  smfmullem4  46803  smfpimbor1lem1  46807