Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > domtr | Structured version Visualization version GIF version |
Description: Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94. (Contributed by NM, 4-Jun-1998.) (Revised by Mario Carneiro, 15-Nov-2014.) |
Ref | Expression |
---|---|
domtr | ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reldom 8515 | . 2 ⊢ Rel ≼ | |
2 | vex 3497 | . . . 4 ⊢ 𝑦 ∈ V | |
3 | 2 | brdom 8521 | . . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦) |
4 | vex 3497 | . . . 4 ⊢ 𝑧 ∈ V | |
5 | 4 | brdom 8521 | . . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧) |
6 | exdistrv 1956 | . . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧)) | |
7 | f1co 6585 | . . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧) | |
8 | 7 | ancoms 461 | . . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧) |
9 | vex 3497 | . . . . . . . . 9 ⊢ 𝑓 ∈ V | |
10 | vex 3497 | . . . . . . . . 9 ⊢ 𝑔 ∈ V | |
11 | 9, 10 | coex 7635 | . . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V |
12 | f1eq1 6570 | . . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)) | |
13 | 11, 12 | spcev 3607 | . . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧) |
14 | 8, 13 | syl 17 | . . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧) |
15 | 4 | brdom 8521 | . . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧) |
16 | 14, 15 | sylibr 236 | . . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧) |
17 | 16 | exlimivv 1933 | . . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧) |
18 | 6, 17 | sylbir 237 | . . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧) |
19 | 3, 5, 18 | syl2anb 599 | . 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧) |
20 | 1, 19 | vtoclr 5615 | 1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∃wex 1780 class class class wbr 5066 ∘ ccom 5559 –1-1→wf1 6352 ≼ cdom 8507 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-dom 8511 |
This theorem is referenced by: endomtr 8567 domentr 8568 cnvct 8586 ssct 8598 undom 8605 sdomdomtr 8650 domsdomtr 8652 xpen 8680 unxpdom2 8726 sucxpdom 8727 fidomdm 8801 hartogs 9008 harword 9029 unxpwdom 9053 harcard 9407 infxpenlem 9439 xpct 9442 indcardi 9467 fodomfi2 9486 infpwfien 9488 inffien 9489 djudoml 9610 djuinf 9614 infdju1 9615 djulepw 9618 unctb 9627 infdjuabs 9628 infdju 9630 infdif 9631 infdif2 9632 infxp 9637 infmap2 9640 fictb 9667 cfslb2n 9690 isfin32i 9787 fin1a2lem12 9833 hsmexlem1 9848 dmct 9946 brdom3 9950 brdom5 9951 brdom4 9952 imadomg 9956 fimact 9957 fnct 9959 mptct 9960 iundomg 9963 uniimadom 9966 ondomon 9985 unirnfdomd 9989 alephval2 9994 iunctb 9996 alephexp1 10001 alephreg 10004 cfpwsdom 10006 gchdomtri 10051 canthnum 10071 canthp1lem1 10074 canthp1 10076 pwfseqlem5 10085 pwxpndom2 10087 pwxpndom 10088 pwdjundom 10089 gchdjuidm 10090 gchxpidm 10091 gchpwdom 10092 gchaclem 10100 gchhar 10101 inar1 10197 rankcf 10199 grudomon 10239 grothac 10252 rpnnen 15580 cctop 21614 1stcfb 22053 2ndcredom 22058 2ndc1stc 22059 1stcrestlem 22060 2ndcctbss 22063 2ndcdisj2 22065 2ndcomap 22066 2ndcsep 22067 dis2ndc 22068 hauspwdom 22109 tx1stc 22258 tx2ndc 22259 met2ndci 23132 opnreen 23439 rectbntr0 23440 uniiccdif 24179 dyadmbl 24201 opnmblALT 24204 mbfimaopnlem 24256 abrexdomjm 30267 mptctf 30453 locfinreflem 31104 sigaclci 31391 omsmeas 31581 sibfof 31598 abrexdom 35020 heiborlem3 35106 ttac 39653 idomsubgmo 39818 pr2dom 39913 tr3dom 39914 uzct 41345 omeiunle 42819 smfaddlem2 43060 smflimlem6 43072 smfmullem4 43089 smfpimbor1lem1 43093 |
Copyright terms: Public domain | W3C validator |