| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: A set that dominates ordinal 2 has at least 2 different members. |
| Ref | Expression |
|---|---|
| 2dom.1 |
|
| Ref | Expression |
|---|---|
| 2dom |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df2o2 4199 |
. . . 4
| |
| 2 | 1 | breq1i 2681 |
. . 3
|
| 3 | 2dom.1 |
. . . 4
| |
| 4 | 3 | brdom 4439 |
. . 3
|
| 5 | 2, 4 | bitri 180 |
. 2
|
| 6 | eqeq1 1528 |
. . . . . 6
| |
| 7 | 6 | notbid 622 |
. . . . 5
|
| 8 | eqeq2 1531 |
. . . . . 6
| |
| 9 | 8 | notbid 622 |
. . . . 5
|
| 10 | 7, 9 | rcla42ev 1928 |
. . . 4
|
| 11 | f1f 3722 |
. . . . 5
| |
| 12 | 0ex 2766 |
. . . . . . 7
| |
| 13 | 12 | prid1 2504 |
. . . . . 6
|
| 14 | ffvelrn 3871 |
. . . . . 6
| |
| 15 | 13, 14 | mpan2 708 |
. . . . 5
|
| 16 | 11, 15 | syl 10 |
. . . 4
|
| 17 | p0ex 2826 |
. . . . . . 7
| |
| 18 | 17 | prid2 2505 |
. . . . . 6
|
| 19 | ffvelrn 3871 |
. . . . . 6
| |
| 20 | 18, 19 | mpan2 708 |
. . . . 5
|
| 21 | 11, 20 | syl 10 |
. . . 4
|
| 22 | 0nep0 2792 |
. . . . . 6
| |
| 23 | df-ne 1634 |
. . . . . 6
| |
| 24 | 22, 23 | mpbi 196 |
. . . . 5
|
| 25 | 13, 18 | pm3.2i 292 |
. . . . . 6
|
| 26 | f1fveq 3934 |
. . . . . 6
| |
| 27 | 25, 26 | mpan2 708 |
. . . . 5
|
| 28 | 24, 27 | mtbiri 729 |
. . . 4
|
| 29 | 10, 16, 21, 28 | syl3anc 870 |
. . 3
|
| 30 | 29 | 19.23aiv 1337 |
. 2
|
| 31 | 5, 30 | sylbi 206 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: unxpdomlem 4908 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1003 ax-gen 1004 ax-8 1005 ax-9 1006 ax-10 1007 ax-11 1008 ax-12 1009 ax-13 1010 ax-14 1011 ax-17 1012 ax-4 1014 ax-5o 1016 ax-6o 1019 ax-9o 1164 ax-10o 1182 ax-16 1252 ax-11o 1260 ax-ext 1504 ax-sep 2758 ax-nul 2765 ax-pow 2798 ax-pr 2835 ax-un 2922 |
| This theorem depends on definitions: df-bi 154 df-or 231 df-an 232 df-3an 789 df-ex 1022 df-sb 1214 df-eu 1424 df-mo 1425 df-clab 1510 df-cleq 1515 df-clel 1518 df-ne 1634 df-ral 1696 df-rex 1697 df-v 1859 df-dif 2100 df-un 2101 df-in 2102 df-ss 2104 df-nul 2332 df-pw 2454 df-sn 2464 df-pr 2465 df-op 2468 df-uni 2558 df-br 2675 df-opab 2722 df-id 2891 df-suc 3011 df-xp 3241 df-rel 3242 df-cnv 3243 df-co 3244 df-dm 3245 df-rn 3246 df-res 3247 df-ima 3248 df-fun 3249 df-fn 3250 df-f 3251 df-f1 3252 df-fv 3255 df-1o 4191 df-2o 4192 df-dom 4430 |