New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > pw1eqadj | Unicode version |
Description: A condition for a unit power class to work out to an adjunction. (Contributed by SF, 26-Jan-2015.) |
Ref | Expression |
---|---|
pw1eqadj.1 | |
pw1eqadj.2 |
Ref | Expression |
---|---|
pw1eqadj | 1 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unieq 3900 | . . . . 5 1 1 | |
2 | unipw1 4325 | . . . . 5 1 | |
3 | uniun 3910 | . . . . 5 | |
4 | 1, 2, 3 | 3eqtr3g 2408 | . . . 4 1 |
5 | pw1eqadj.2 | . . . . . . 7 | |
6 | 5 | unisn 3907 | . . . . . 6 |
7 | pw1ss1c 4158 | . . . . . . . 8 1 1c | |
8 | ssun2 3427 | . . . . . . . . . 10 | |
9 | 5 | snid 3760 | . . . . . . . . . 10 |
10 | 8, 9 | sselii 3270 | . . . . . . . . 9 |
11 | eleq2 2414 | . . . . . . . . 9 1 1 | |
12 | 10, 11 | mpbiri 224 | . . . . . . . 8 1 1 |
13 | 7, 12 | sseldi 3271 | . . . . . . 7 1 1c |
14 | el1c 4139 | . . . . . . . 8 1c | |
15 | vex 2862 | . . . . . . . . . . . . 13 | |
16 | 15 | unisn 3907 | . . . . . . . . . . . 12 |
17 | 16 | sneqi 3745 | . . . . . . . . . . 11 |
18 | 17 | eqcomi 2357 | . . . . . . . . . 10 |
19 | id 19 | . . . . . . . . . 10 | |
20 | unieq 3900 | . . . . . . . . . . 11 | |
21 | 20 | sneqd 3746 | . . . . . . . . . 10 |
22 | 18, 19, 21 | 3eqtr4a 2411 | . . . . . . . . 9 |
23 | 22 | exlimiv 1634 | . . . . . . . 8 |
24 | 14, 23 | sylbi 187 | . . . . . . 7 1c |
25 | 13, 24 | syl 15 | . . . . . 6 1 |
26 | 6, 25 | syl5eq 2397 | . . . . 5 1 |
27 | 26 | uneq2d 3418 | . . . 4 1 |
28 | 4, 27 | eqtrd 2385 | . . 3 1 |
29 | ssun1 3426 | . . . . . 6 | |
30 | sseq2 3293 | . . . . . 6 1 1 | |
31 | 29, 30 | mpbiri 224 | . . . . 5 1 1 |
32 | 31, 7 | syl6ss 3284 | . . . 4 1 1c |
33 | eqpw1uni 4330 | . . . 4 1c 1 | |
34 | 32, 33 | syl 15 | . . 3 1 1 |
35 | pw1eqadj.1 | . . . . 5 | |
36 | 35 | uniex 4317 | . . . 4 |
37 | 5 | uniex 4317 | . . . 4 |
38 | sneq 3744 | . . . . . . 7 | |
39 | uneq12 3413 | . . . . . . 7 | |
40 | 38, 39 | sylan2 460 | . . . . . 6 |
41 | 40 | eqeq2d 2364 | . . . . 5 |
42 | pw1eq 4143 | . . . . . . 7 1 1 | |
43 | 42 | eqeq2d 2364 | . . . . . 6 1 1 |
44 | 43 | adantr 451 | . . . . 5 1 1 |
45 | 38 | eqeq2d 2364 | . . . . . 6 |
46 | 45 | adantl 452 | . . . . 5 |
47 | 41, 44, 46 | 3anbi123d 1252 | . . . 4 1 1 |
48 | 36, 37, 47 | spc2ev 2947 | . . 3 1 1 |
49 | 28, 34, 25, 48 | syl3anc 1182 | . 2 1 1 |
50 | pw1un 4163 | . . . . 5 1 1 1 | |
51 | vex 2862 | . . . . . . 7 | |
52 | 51 | pw1sn 4165 | . . . . . 6 1 |
53 | 52 | uneq2i 3415 | . . . . 5 1 1 1 |
54 | 50, 53 | eqtri 2373 | . . . 4 1 1 |
55 | pw1eq 4143 | . . . . . 6 1 1 | |
56 | sneq 3744 | . . . . . . 7 | |
57 | uneq12 3413 | . . . . . . 7 1 1 | |
58 | 56, 57 | sylan2 460 | . . . . . 6 1 1 |
59 | 55, 58 | eqeqan12d 2368 | . . . . 5 1 1 1 1 |
60 | 59 | 3impb 1147 | . . . 4 1 1 1 1 |
61 | 54, 60 | mpbiri 224 | . . 3 1 1 |
62 | 61 | exlimivv 1635 | . 2 1 1 |
63 | 49, 62 | impbii 180 | 1 1 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 wa 358 w3a 934 wex 1541 wceq 1642 wcel 1710 cvv 2859 cun 3207 wss 3257 csn 3737 cuni 3891 1cc1c 4134 1 cpw1 4135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4078 ax-xp 4079 ax-cnv 4080 ax-1c 4081 ax-sset 4082 ax-si 4083 ax-typlower 4086 ax-sn 4087 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-v 2861 df-sbc 3047 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-ss 3259 df-nul 3551 df-pw 3724 df-sn 3741 df-pr 3742 df-uni 3892 df-opk 4058 df-1c 4136 df-pw1 4137 df-uni1 4138 df-xpk 4185 df-cnvk 4186 df-imak 4189 df-p6 4191 df-sik 4192 df-ssetk 4193 |
This theorem is referenced by: ncfinlower 4483 sfindbl 4530 |
Copyright terms: Public domain | W3C validator |