![]() |
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 8115 | . 2 ⊢ Rel ≼ | |
2 | vex 3354 | . . . 4 ⊢ 𝑦 ∈ V | |
3 | 2 | brdom 8121 | . . 3 ⊢ (𝑥 ≼ 𝑦 ↔ ∃𝑔 𝑔:𝑥–1-1→𝑦) |
4 | vex 3354 | . . . 4 ⊢ 𝑧 ∈ V | |
5 | 4 | brdom 8121 | . . 3 ⊢ (𝑦 ≼ 𝑧 ↔ ∃𝑓 𝑓:𝑦–1-1→𝑧) |
6 | eeanv 2344 | . . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) ↔ (∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧)) | |
7 | f1co 6251 | . . . . . . . 8 ⊢ ((𝑓:𝑦–1-1→𝑧 ∧ 𝑔:𝑥–1-1→𝑦) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧) | |
8 | 7 | ancoms 455 | . . . . . . 7 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → (𝑓 ∘ 𝑔):𝑥–1-1→𝑧) |
9 | vex 3354 | . . . . . . . . 9 ⊢ 𝑓 ∈ V | |
10 | vex 3354 | . . . . . . . . 9 ⊢ 𝑔 ∈ V | |
11 | 9, 10 | coex 7265 | . . . . . . . 8 ⊢ (𝑓 ∘ 𝑔) ∈ V |
12 | f1eq1 6236 | . . . . . . . 8 ⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ:𝑥–1-1→𝑧 ↔ (𝑓 ∘ 𝑔):𝑥–1-1→𝑧)) | |
13 | 11, 12 | spcev 3451 | . . . . . . 7 ⊢ ((𝑓 ∘ 𝑔):𝑥–1-1→𝑧 → ∃ℎ ℎ:𝑥–1-1→𝑧) |
14 | 8, 13 | syl 17 | . . . . . 6 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → ∃ℎ ℎ:𝑥–1-1→𝑧) |
15 | 4 | brdom 8121 | . . . . . 6 ⊢ (𝑥 ≼ 𝑧 ↔ ∃ℎ ℎ:𝑥–1-1→𝑧) |
16 | 14, 15 | sylibr 224 | . . . . 5 ⊢ ((𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧) |
17 | 16 | exlimivv 2012 | . . . 4 ⊢ (∃𝑔∃𝑓(𝑔:𝑥–1-1→𝑦 ∧ 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧) |
18 | 6, 17 | sylbir 225 | . . 3 ⊢ ((∃𝑔 𝑔:𝑥–1-1→𝑦 ∧ ∃𝑓 𝑓:𝑦–1-1→𝑧) → 𝑥 ≼ 𝑧) |
19 | 3, 5, 18 | syl2anb 585 | . 2 ⊢ ((𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧) → 𝑥 ≼ 𝑧) |
20 | 1, 19 | vtoclr 5304 | 1 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 ∃wex 1852 class class class wbr 4786 ∘ ccom 5253 –1-1→wf1 6028 ≼ cdom 8107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7096 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-op 4323 df-uni 4575 df-br 4787 df-opab 4847 df-id 5157 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036 df-dom 8111 |
This theorem is referenced by: endomtr 8167 domentr 8168 cnvct 8186 ssct 8197 undom 8204 sdomdomtr 8249 domsdomtr 8251 xpen 8279 unxpdom2 8324 sucxpdom 8325 fidomdm 8399 hartogs 8605 harword 8626 unxpwdom 8650 harcard 9004 infxpenlem 9036 xpct 9039 indcardi 9064 fodomfi2 9083 infpwfien 9085 inffien 9086 cdadom3 9212 cdainf 9216 infcda1 9217 cdalepw 9220 unctb 9229 infcdaabs 9230 infcda 9232 infdif 9233 infdif2 9234 infxp 9239 infmap2 9242 fictb 9269 cfslb2n 9292 isfin32i 9389 fin1a2lem12 9435 hsmexlem1 9450 dmct 9548 brdom3 9552 brdom5 9553 brdom4 9554 imadomg 9558 fimact 9559 fnct 9561 mptct 9562 iundomg 9565 uniimadom 9568 ondomon 9587 unirnfdomd 9591 alephval2 9596 iunctb 9598 alephexp1 9603 alephreg 9606 cfpwsdom 9608 gchdomtri 9653 canthnum 9673 canthp1lem1 9676 canthp1 9678 pwfseqlem5 9687 pwxpndom2 9689 pwxpndom 9690 pwcdandom 9691 gchcdaidm 9692 gchxpidm 9693 gchpwdom 9694 gchaclem 9702 gchhar 9703 inar1 9799 rankcf 9801 grudomon 9841 grothac 9854 rpnnen 15162 cctop 21031 1stcfb 21469 2ndcredom 21474 2ndc1stc 21475 1stcrestlem 21476 2ndcctbss 21479 2ndcdisj2 21481 2ndcomap 21482 2ndcsep 21483 dis2ndc 21484 hauspwdom 21525 tx1stc 21674 tx2ndc 21675 met2ndci 22547 opnreen 22854 rectbntr0 22855 uniiccdif 23566 dyadmbl 23588 opnmblALT 23591 mbfimaopnlem 23642 abrexdomjm 29683 mptctf 29835 locfinreflem 30247 sigaclci 30535 omsmeas 30725 sibfof 30742 abrexdom 33857 heiborlem3 33944 ttac 38129 idomsubgmo 38302 uzct 39753 omeiunle 41251 smfaddlem2 41492 smflimlem6 41504 smfmullem4 41521 smfpimbor1lem1 41525 |
Copyright terms: Public domain | W3C validator |