![]() |
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 8892 | . 2 ⊢ Rel ≼ | |
2 | vex 3448 | . . . 4 ⊢ 𝑦 ∈ V | |
3 | 2 | brdom 8903 | . . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦) |
4 | vex 3448 | . . . 4 ⊢ 𝑧 ∈ V | |
5 | 4 | brdom 8903 | . . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧) |
6 | exdistrv 1960 | . . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧)) | |
7 | f1co 6751 | . . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧) | |
8 | 7 | ancoms 460 | . . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧) |
9 | vex 3448 | . . . . . . . . 9 ⊢ 𝑓 ∈ V | |
10 | vex 3448 | . . . . . . . . 9 ⊢ 𝑔 ∈ V | |
11 | 9, 10 | coex 7868 | . . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V |
12 | f1eq1 6734 | . . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)) | |
13 | 11, 12 | spcev 3564 | . . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧) |
14 | 8, 13 | syl 17 | . . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧) |
15 | 4 | brdom 8903 | . . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧) |
16 | 14, 15 | sylibr 233 | . . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧) |
17 | 16 | exlimivv 1936 | . . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧) |
18 | 6, 17 | sylbir 234 | . . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧) |
19 | 3, 5, 18 | syl2anb 599 | . 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧) |
20 | 1, 19 | vtoclr 5696 | 1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∃wex 1782 class class class wbr 5106 ∘ ccom 5638 –1-1→wf1 6494 ≼ cdom 8884 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5257 ax-nul 5264 ax-pow 5321 ax-pr 5385 ax-un 7673 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-id 5532 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-dom 8888 |
This theorem is referenced by: endomtr 8955 domentr 8956 cnvct 8981 ssctOLD 8999 undomOLD 9007 sdomdomtr 9057 domsdomtr 9059 xpen 9087 unxpdom2 9201 sucxpdom 9202 fidomdm 9276 hartogs 9485 harword 9504 unxpwdom 9530 harcard 9919 infxpenlem 9954 xpct 9957 indcardi 9982 fodomfi2 10001 infpwfien 10003 inffien 10004 djudoml 10125 djuinf 10129 infdju1 10130 djulepw 10133 unctb 10146 infdjuabs 10147 infdju 10149 infdif 10150 infdif2 10151 infxp 10156 infmap2 10159 fictb 10186 cfslb2n 10209 isfin32i 10306 fin1a2lem12 10352 hsmexlem1 10367 dmct 10465 brdom3 10469 brdom5 10470 brdom4 10471 imadomg 10475 fimact 10476 fnct 10478 mptct 10479 iundomg 10482 uniimadom 10485 ondomon 10504 unirnfdomd 10508 alephval2 10513 iunctb 10515 alephexp1 10520 alephreg 10523 cfpwsdom 10525 gchdomtri 10570 canthnum 10590 canthp1lem1 10593 canthp1 10595 pwfseqlem5 10604 pwxpndom2 10606 pwxpndom 10607 pwdjundom 10608 gchdjuidm 10609 gchxpidm 10610 gchpwdom 10611 gchaclem 10619 gchhar 10620 inar1 10716 rankcf 10718 grudomon 10758 grothac 10771 rpnnen 16114 cctop 22372 1stcfb 22812 2ndcredom 22817 2ndc1stc 22818 1stcrestlem 22819 2ndcctbss 22822 2ndcdisj2 22824 2ndcomap 22825 2ndcsep 22826 dis2ndc 22827 hauspwdom 22868 tx1stc 23017 tx2ndc 23018 met2ndci 23894 opnreen 24210 rectbntr0 24211 uniiccdif 24958 dyadmbl 24980 opnmblALT 24983 mbfimaopnlem 25035 abrexdomjm 31476 mptctf 31681 locfinreflem 32478 sigaclci 32788 omsmeas 32980 sibfof 32997 abrexdom 36235 heiborlem3 36318 ttac 41403 idomsubgmo 41568 safesnsupfidom1o 41777 pr2dom 41887 tr3dom 41888 uzct 43359 rn1st 43589 omeiunle 44844 smfaddlem2 45091 smflimlem6 45103 smfmullem4 45121 smfpimbor1lem1 45125 |
Copyright terms: Public domain | W3C validator |