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 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 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |