Step | Hyp | Ref
| Expression |
1 | | elat2 31593 |
. . . 4
β’ (π΄ β HAtoms β (π΄ β
Cβ β§ (π΄ β 0β β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β))))) |
2 | | chne0 30747 |
. . . . . 6
β’ (π΄ β
Cβ β (π΄ β 0β β
βπ₯ β π΄ π₯ β 0β)) |
3 | | nfv 1918 |
. . . . . . 7
β’
β²π₯ π΄ β
Cβ |
4 | | nfv 1918 |
. . . . . . . 8
β’
β²π₯βπ¦ β Cβ
(π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) |
5 | | nfre1 3283 |
. . . . . . . 8
β’
β²π₯βπ₯ β β (π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯}))) |
6 | 4, 5 | nfim 1900 |
. . . . . . 7
β’
β²π₯(βπ¦ β Cβ
(π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) β βπ₯ β β (π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯})))) |
7 | | chel 30483 |
. . . . . . . . . . 11
β’ ((π΄ β
Cβ β§ π₯ β π΄) β π₯ β β) |
8 | 7 | adantrr 716 |
. . . . . . . . . 10
β’ ((π΄ β
Cβ β§ (π₯ β π΄ β§ π₯ β 0β)) β π₯ β
β) |
9 | 8 | adantrr 716 |
. . . . . . . . 9
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β π₯ β
β) |
10 | | simprlr 779 |
. . . . . . . . 9
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β π₯ β
0β) |
11 | | h1dn0 30805 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π₯ β 0β)
β (β₯β(β₯β{π₯})) β
0β) |
12 | 7, 11 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π΄ β
Cβ β§ π₯ β π΄) β§ π₯ β 0β) β
(β₯β(β₯β{π₯})) β
0β) |
13 | 12 | anasss 468 |
. . . . . . . . . . . 12
β’ ((π΄ β
Cβ β§ (π₯ β π΄ β§ π₯ β 0β)) β
(β₯β(β₯β{π₯})) β
0β) |
14 | 13 | adantrr 716 |
. . . . . . . . . . 11
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β
(β₯β(β₯β{π₯})) β
0β) |
15 | | ch1dle 31605 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
Cβ β§ π₯ β π΄) β
(β₯β(β₯β{π₯})) β π΄) |
16 | | snssi 4812 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β {π₯} β
β) |
17 | | occl 30557 |
. . . . . . . . . . . . . . . . . 18
β’ ({π₯} β β β
(β₯β{π₯}) β
Cβ ) |
18 | 7, 16, 17 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β
Cβ β§ π₯ β π΄) β (β₯β{π₯}) β Cβ
) |
19 | | choccl 30559 |
. . . . . . . . . . . . . . . . 17
β’
((β₯β{π₯})
β Cβ β
(β₯β(β₯β{π₯})) β Cβ
) |
20 | | sseq1 4008 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ =
(β₯β(β₯β{π₯})) β (π¦ β π΄ β (β₯β(β₯β{π₯})) β π΄)) |
21 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ =
(β₯β(β₯β{π₯})) β (π¦ = π΄ β (β₯β(β₯β{π₯})) = π΄)) |
22 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ =
(β₯β(β₯β{π₯})) β (π¦ = 0β β
(β₯β(β₯β{π₯})) = 0β)) |
23 | 21, 22 | orbi12d 918 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ =
(β₯β(β₯β{π₯})) β ((π¦ = π΄ β¨ π¦ = 0β) β
((β₯β(β₯β{π₯})) = π΄ β¨ (β₯β(β₯β{π₯})) =
0β))) |
24 | 20, 23 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ =
(β₯β(β₯β{π₯})) β ((π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) β
((β₯β(β₯β{π₯})) β π΄ β
((β₯β(β₯β{π₯})) = π΄ β¨ (β₯β(β₯β{π₯})) =
0β)))) |
25 | 24 | rspcv 3609 |
. . . . . . . . . . . . . . . . 17
β’
((β₯β(β₯β{π₯})) β Cβ
β (βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) β
((β₯β(β₯β{π₯})) β π΄ β
((β₯β(β₯β{π₯})) = π΄ β¨ (β₯β(β₯β{π₯})) =
0β)))) |
26 | 18, 19, 25 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
Cβ β§ π₯ β π΄) β (βπ¦ β Cβ
(π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) β
((β₯β(β₯β{π₯})) β π΄ β
((β₯β(β₯β{π₯})) = π΄ β¨ (β₯β(β₯β{π₯})) =
0β)))) |
27 | 15, 26 | mpid 44 |
. . . . . . . . . . . . . . 15
β’ ((π΄ β
Cβ β§ π₯ β π΄) β (βπ¦ β Cβ
(π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) β
((β₯β(β₯β{π₯})) = π΄ β¨ (β₯β(β₯β{π₯})) =
0β))) |
28 | 27 | impr 456 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
Cβ β§ (π₯ β π΄ β§ βπ¦ β Cβ
(π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β
((β₯β(β₯β{π₯})) = π΄ β¨ (β₯β(β₯β{π₯})) =
0β)) |
29 | 28 | adantrlr 722 |
. . . . . . . . . . . . 13
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β
((β₯β(β₯β{π₯})) = π΄ β¨ (β₯β(β₯β{π₯})) =
0β)) |
30 | 29 | ord 863 |
. . . . . . . . . . . 12
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β (Β¬
(β₯β(β₯β{π₯})) = π΄ β (β₯β(β₯β{π₯})) =
0β)) |
31 | | nne 2945 |
. . . . . . . . . . . 12
β’ (Β¬
(β₯β(β₯β{π₯})) β 0β β
(β₯β(β₯β{π₯})) = 0β) |
32 | 30, 31 | syl6ibr 252 |
. . . . . . . . . . 11
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β (Β¬
(β₯β(β₯β{π₯})) = π΄ β Β¬
(β₯β(β₯β{π₯})) β
0β)) |
33 | 14, 32 | mt4d 117 |
. . . . . . . . . 10
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β
(β₯β(β₯β{π₯})) = π΄) |
34 | 33 | eqcomd 2739 |
. . . . . . . . 9
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β π΄ =
(β₯β(β₯β{π₯}))) |
35 | | rspe 3247 |
. . . . . . . . 9
β’ ((π₯ β β β§ (π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯})))) β βπ₯ β β (π₯ β 0β β§ π΄ =
(β₯β(β₯β{π₯})))) |
36 | 9, 10, 34, 35 | syl12anc 836 |
. . . . . . . 8
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β
βπ₯ β β
(π₯ β
0β β§ π΄ = (β₯β(β₯β{π₯})))) |
37 | 36 | exp44 439 |
. . . . . . 7
β’ (π΄ β
Cβ β (π₯ β π΄ β (π₯ β 0β β
(βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) β βπ₯ β β (π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯}))))))) |
38 | 3, 6, 37 | rexlimd 3264 |
. . . . . 6
β’ (π΄ β
Cβ β (βπ₯ β π΄ π₯ β 0β β
(βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) β βπ₯ β β (π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯})))))) |
39 | 2, 38 | sylbid 239 |
. . . . 5
β’ (π΄ β
Cβ β (π΄ β 0β β
(βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) β βπ₯ β β (π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯})))))) |
40 | 39 | imp32 420 |
. . . 4
β’ ((π΄ β
Cβ β§ (π΄ β 0β β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β
βπ₯ β β
(π₯ β
0β β§ π΄ = (β₯β(β₯β{π₯})))) |
41 | 1, 40 | sylbi 216 |
. . 3
β’ (π΄ β HAtoms β
βπ₯ β β
(π₯ β
0β β§ π΄ = (β₯β(β₯β{π₯})))) |
42 | | h1da 31602 |
. . . . . . 7
β’ ((π₯ β β β§ π₯ β 0β)
β (β₯β(β₯β{π₯})) β HAtoms) |
43 | | eleq1 2822 |
. . . . . . 7
β’ (π΄ =
(β₯β(β₯β{π₯})) β (π΄ β HAtoms β
(β₯β(β₯β{π₯})) β HAtoms)) |
44 | 42, 43 | imbitrrid 245 |
. . . . . 6
β’ (π΄ =
(β₯β(β₯β{π₯})) β ((π₯ β β β§ π₯ β 0β) β π΄ β
HAtoms)) |
45 | 44 | expdcom 416 |
. . . . 5
β’ (π₯ β β β (π₯ β 0β
β (π΄ =
(β₯β(β₯β{π₯})) β π΄ β HAtoms))) |
46 | 45 | impd 412 |
. . . 4
β’ (π₯ β β β ((π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯}))) β π΄ β HAtoms)) |
47 | 46 | rexlimiv 3149 |
. . 3
β’
(βπ₯ β
β (π₯ β
0β β§ π΄ = (β₯β(β₯β{π₯}))) β π΄ β HAtoms) |
48 | 41, 47 | impbii 208 |
. 2
β’ (π΄ β HAtoms β
βπ₯ β β
(π₯ β
0β β§ π΄ = (β₯β(β₯β{π₯})))) |
49 | | spansn 30812 |
. . . . 5
β’ (π₯ β β β
(spanβ{π₯}) =
(β₯β(β₯β{π₯}))) |
50 | 49 | eqeq2d 2744 |
. . . 4
β’ (π₯ β β β (π΄ = (spanβ{π₯}) β π΄ = (β₯β(β₯β{π₯})))) |
51 | 50 | anbi2d 630 |
. . 3
β’ (π₯ β β β ((π₯ β 0β β§
π΄ = (spanβ{π₯})) β (π₯ β 0β β§ π΄ =
(β₯β(β₯β{π₯}))))) |
52 | 51 | rexbiia 3093 |
. 2
β’
(βπ₯ β
β (π₯ β
0β β§ π΄ = (spanβ{π₯})) β βπ₯ β β (π₯ β 0β β§ π΄ =
(β₯β(β₯β{π₯})))) |
53 | 48, 52 | bitr4i 278 |
1
β’ (π΄ β HAtoms β
βπ₯ β β
(π₯ β
0β β§ π΄ = (spanβ{π₯}))) |