Theorem domtr 9029

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 8973	. 2 ⊢ Rel ≼
2		vex 3467	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8983	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3467	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8983	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		exdistrv 1954	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6795	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 458	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3467	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3467	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7934	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6779	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3589	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8983	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 234	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 1931	. . . 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 5728	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1778   class class class wbr 5123   ∘ ccom 5669  –1-1→wf1 6538   ≼ cdom 8965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  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 4888  df-br 5124  df-opab 5186  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-dom 8969

This theorem is referenced by:  endomtr  9034  domentr  9035  cnvct  9056  ssctOLD  9074  undomOLD  9082  sdomdomtr  9132  domsdomtr  9134  xpen  9162  unxpdom2  9272  sucxpdom  9273  fidomdm  9356  hartogs  9566  harword  9585  unxpwdom  9611  harcard  10000  infxpenlem  10035  xpct  10038  indcardi  10063  fodomfi2  10082  infpwfien  10084  inffien  10085  djudoml  10207  djuinf  10211  infdju1  10212  djulepw  10215  unctb  10226  infdjuabs  10227  infdju  10229  infdif  10230  infdif2  10231  infxp  10236  infmap2  10239  fictb  10266  cfslb2n  10290  isfin32i  10387  fin1a2lem12  10433  hsmexlem1  10448  dmct  10546  brdom3  10550  brdom5  10551  brdom4  10552  imadomg  10556  fimact  10557  fnct  10559  mptct  10560  iundomg  10563  uniimadom  10566  ondomon  10585  unirnfdomd  10589  alephval2  10594  iunctb  10596  alephexp1  10601  alephreg  10604  cfpwsdom  10606  gchdomtri  10651  canthnum  10671  canthp1lem1  10674  canthp1  10676  pwfseqlem5  10685  pwxpndom2  10687  pwxpndom  10688  pwdjundom  10689  gchdjuidm  10690  gchxpidm  10691  gchpwdom  10692  gchaclem  10700  gchhar  10701  inar1  10797  rankcf  10799  grudomon  10839  grothac  10852  rpnnen  16245  cctop  22960  1stcfb  23399  2ndcredom  23404  2ndc1stc  23405  1stcrestlem  23406  2ndcctbss  23409  2ndcdisj2  23411  2ndcomap  23412  2ndcsep  23413  dis2ndc  23414  hauspwdom  23455  tx1stc  23604  tx2ndc  23605  met2ndci  24479  opnreen  24789  rectbntr0  24790  uniiccdif  25549  dyadmbl  25571  opnmblALT  25574  mbfimaopnlem  25626  abrexdomjm  32454  mptctf  32664  locfinreflem  33798  sigaclci  34092  omsmeas  34284  sibfof  34301  abrexdom  37696  heiborlem3  37779  imadomfi  41962  ttac  43011  idomsubgmo  43168  safesnsupfidom1o  43392  pr2dom  43502  tr3dom  43503  uzct  45025  rn1st  45237  omeiunle  46489  smfaddlem2  46736  smflimlem6  46748  smfmullem4  46766  smfpimbor1lem1  46770