Theorem domtr 8213

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 8166	. 2 ⊢ Rel ≼
2		vex 3353	. . . 4 ⊢ 𝑦 ∈ V
3	2	brdom 8172	. . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦)
4		vex 3353	. . . 4 ⊢ 𝑧 ∈ V
5	4	brdom 8172	. . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧)
6		eeanv 2346	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧))
7		f1co 6293	. . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
8	7	ancoms 450	. . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)
9		vex 3353	. . . . . . . . 9 ⊢ 𝑓 ∈ V
10		vex 3353	. . . . . . . . 9 ⊢ 𝑔 ∈ V
11	9, 10	coex 7316	. . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V
12		f1eq1 6278	. . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧))
13	11, 12	spcev 3452	. . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧)
14	8, 13	syl 17	. . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧)
15	4	brdom 8172	. . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧)
16	14, 15	sylibr 225	. . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
17	16	exlimivv 2027	. . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
18	6, 17	sylbir 226	. . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧)
19	3, 5, 18	syl2anb 591	. 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧)
20	1, 19	vtoclr 5334	1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶)

Syntax hints:   → wi 4   ∧ wa 384  ∃wex 1874   class class class wbr 4809   ∘ ccom 5281  –1-1→wf1 6065   ≼ cdom 8158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-dom 8162

This theorem is referenced by:  endomtr  8218  domentr  8219  cnvct  8237  ssct  8248  undom  8255  sdomdomtr  8300  domsdomtr  8302  xpen  8330  unxpdom2  8375  sucxpdom  8376  fidomdm  8450  hartogs  8656  harword  8677  unxpwdom  8701  harcard  9055  infxpenlem  9087  xpct  9090  indcardi  9115  fodomfi2  9134  infpwfien  9136  inffien  9137  cdadom3  9263  cdainf  9267  infcda1  9268  cdalepw  9271  unctb  9280  infcdaabs  9281  infcda  9283  infdif  9284  infdif2  9285  infxp  9290  infmap2  9293  fictb  9320  cfslb2n  9343  isfin32i  9440  fin1a2lem12  9486  hsmexlem1  9501  dmct  9599  brdom3  9603  brdom5  9604  brdom4  9605  imadomg  9609  fimact  9610  fnct  9612  mptct  9613  iundomg  9616  uniimadom  9619  ondomon  9638  unirnfdomd  9642  alephval2  9647  iunctb  9649  alephexp1  9654  alephreg  9657  cfpwsdom  9659  gchdomtri  9704  canthnum  9724  canthp1lem1  9727  canthp1  9729  pwfseqlem5  9738  pwxpndom2  9740  pwxpndom  9741  pwcdandom  9742  gchcdaidm  9743  gchxpidm  9744  gchpwdom  9745  gchaclem  9753  gchhar  9754  inar1  9850  rankcf  9852  grudomon  9892  grothac  9905  rpnnen  15238  cctop  21090  1stcfb  21528  2ndcredom  21533  2ndc1stc  21534  1stcrestlem  21535  2ndcctbss  21538  2ndcdisj2  21540  2ndcomap  21541  2ndcsep  21542  dis2ndc  21543  hauspwdom  21584  tx1stc  21733  tx2ndc  21734  met2ndci  22606  opnreen  22913  rectbntr0  22914  uniiccdif  23636  dyadmbl  23658  opnmblALT  23661  mbfimaopnlem  23713  abrexdomjm  29794  mptctf  29944  locfinreflem  30354  sigaclci  30642  omsmeas  30832  sibfof  30849  abrexdom  33948  heiborlem3  34034  ttac  38280  idomsubgmo  38453  uzct  39883  omeiunle  41371  smfaddlem2  41612  smflimlem6  41624  smfmullem4  41641  smfpimbor1lem1  41645