Step | Hyp | Ref
| Expression |
1 | | elat2 31858 |
. . . 4
β’ (π΄ β HAtoms β (π΄ β
Cβ β§ (π΄ β 0β β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β))))) |
2 | | chne0 31012 |
. . . . . 6
β’ (π΄ β
Cβ β (π΄ β 0β β
βπ₯ β π΄ π₯ β 0β)) |
3 | | nfv 1915 |
. . . . . . 7
β’
β²π₯ π΄ β
Cβ |
4 | | nfv 1915 |
. . . . . . . 8
β’
β²π₯βπ¦ β Cβ
(π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) |
5 | | nfre1 3280 |
. . . . . . . 8
β’
β²π₯βπ₯ β β (π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯}))) |
6 | 4, 5 | nfim 1897 |
. . . . . . 7
β’
β²π₯(βπ¦ β Cβ
(π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) β βπ₯ β β (π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯})))) |
7 | | chel 30748 |
. . . . . . . . . . 11
β’ ((π΄ β
Cβ β§ π₯ β π΄) β π₯ β β) |
8 | 7 | adantrr 713 |
. . . . . . . . . 10
β’ ((π΄ β
Cβ β§ (π₯ β π΄ β§ π₯ β 0β)) β π₯ β
β) |
9 | 8 | adantrr 713 |
. . . . . . . . 9
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β π₯ β
β) |
10 | | simprlr 776 |
. . . . . . . . 9
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β π₯ β
0β) |
11 | | h1dn0 31070 |
. . . . . . . . . . . . . 14
β’ ((π₯ β β β§ π₯ β 0β)
β (β₯β(β₯β{π₯})) β
0β) |
12 | 7, 11 | sylan 578 |
. . . . . . . . . . . . 13
β’ (((π΄ β
Cβ β§ π₯ β π΄) β§ π₯ β 0β) β
(β₯β(β₯β{π₯})) β
0β) |
13 | 12 | anasss 465 |
. . . . . . . . . . . 12
β’ ((π΄ β
Cβ β§ (π₯ β π΄ β§ π₯ β 0β)) β
(β₯β(β₯β{π₯})) β
0β) |
14 | 13 | adantrr 713 |
. . . . . . . . . . 11
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β
(β₯β(β₯β{π₯})) β
0β) |
15 | | ch1dle 31870 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
Cβ β§ π₯ β π΄) β
(β₯β(β₯β{π₯})) β π΄) |
16 | | snssi 4812 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β β β {π₯} β
β) |
17 | | occl 30822 |
. . . . . . . . . . . . . . . . . 18
β’ ({π₯} β β β
(β₯β{π₯}) β
Cβ ) |
18 | 7, 16, 17 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β
Cβ β§ π₯ β π΄) β (β₯β{π₯}) β Cβ
) |
19 | | choccl 30824 |
. . . . . . . . . . . . . . . . 17
β’
((β₯β{π₯})
β Cβ β
(β₯β(β₯β{π₯})) β Cβ
) |
20 | | sseq1 4008 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ =
(β₯β(β₯β{π₯})) β (π¦ β π΄ β (β₯β(β₯β{π₯})) β π΄)) |
21 | | eqeq1 2734 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ =
(β₯β(β₯β{π₯})) β (π¦ = π΄ β (β₯β(β₯β{π₯})) = π΄)) |
22 | | eqeq1 2734 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ =
(β₯β(β₯β{π₯})) β (π¦ = 0β β
(β₯β(β₯β{π₯})) = 0β)) |
23 | 21, 22 | orbi12d 915 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ =
(β₯β(β₯β{π₯})) β ((π¦ = π΄ β¨ π¦ = 0β) β
((β₯β(β₯β{π₯})) = π΄ β¨ (β₯β(β₯β{π₯})) =
0β))) |
24 | 20, 23 | imbi12d 343 |
. . . . . . . . . . . . . . . . . 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 453 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
Cβ β§ (π₯ β π΄ β§ βπ¦ β Cβ
(π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β
((β₯β(β₯β{π₯})) = π΄ β¨ (β₯β(β₯β{π₯})) =
0β)) |
29 | 28 | adantrlr 719 |
. . . . . . . . . . . . 13
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β
((β₯β(β₯β{π₯})) = π΄ β¨ (β₯β(β₯β{π₯})) =
0β)) |
30 | 29 | ord 860 |
. . . . . . . . . . . 12
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β (Β¬
(β₯β(β₯β{π₯})) = π΄ β (β₯β(β₯β{π₯})) =
0β)) |
31 | | nne 2942 |
. . . . . . . . . . . 12
β’ (Β¬
(β₯β(β₯β{π₯})) β 0β β
(β₯β(β₯β{π₯})) = 0β) |
32 | 30, 31 | imbitrrdi 251 |
. . . . . . . . . . 11
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β (Β¬
(β₯β(β₯β{π₯})) = π΄ β Β¬
(β₯β(β₯β{π₯})) β
0β)) |
33 | 14, 32 | mt4d 117 |
. . . . . . . . . 10
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β
(β₯β(β₯β{π₯})) = π΄) |
34 | 33 | eqcomd 2736 |
. . . . . . . . 9
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β π΄ =
(β₯β(β₯β{π₯}))) |
35 | | rspe 3244 |
. . . . . . . . 9
β’ ((π₯ β β β§ (π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯})))) β βπ₯ β β (π₯ β 0β β§ π΄ =
(β₯β(β₯β{π₯})))) |
36 | 9, 10, 34, 35 | syl12anc 833 |
. . . . . . . 8
β’ ((π΄ β
Cβ β§ ((π₯ β π΄ β§ π₯ β 0β) β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β
βπ₯ β β
(π₯ β
0β β§ π΄ = (β₯β(β₯β{π₯})))) |
37 | 36 | exp44 436 |
. . . . . . 7
β’ (π΄ β
Cβ β (π₯ β π΄ β (π₯ β 0β β
(βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) β βπ₯ β β (π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯}))))))) |
38 | 3, 6, 37 | rexlimd 3261 |
. . . . . 6
β’ (π΄ β
Cβ β (βπ₯ β π΄ π₯ β 0β β
(βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) β βπ₯ β β (π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯})))))) |
39 | 2, 38 | sylbid 239 |
. . . . 5
β’ (π΄ β
Cβ β (π΄ β 0β β
(βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)) β βπ₯ β β (π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯})))))) |
40 | 39 | imp32 417 |
. . . 4
β’ ((π΄ β
Cβ β§ (π΄ β 0β β§
βπ¦ β
Cβ (π¦ β π΄ β (π¦ = π΄ β¨ π¦ = 0β)))) β
βπ₯ β β
(π₯ β
0β β§ π΄ = (β₯β(β₯β{π₯})))) |
41 | 1, 40 | sylbi 216 |
. . 3
β’ (π΄ β HAtoms β
βπ₯ β β
(π₯ β
0β β§ π΄ = (β₯β(β₯β{π₯})))) |
42 | | h1da 31867 |
. . . . . . 7
β’ ((π₯ β β β§ π₯ β 0β)
β (β₯β(β₯β{π₯})) β HAtoms) |
43 | | eleq1 2819 |
. . . . . . 7
β’ (π΄ =
(β₯β(β₯β{π₯})) β (π΄ β HAtoms β
(β₯β(β₯β{π₯})) β HAtoms)) |
44 | 42, 43 | imbitrrid 245 |
. . . . . 6
β’ (π΄ =
(β₯β(β₯β{π₯})) β ((π₯ β β β§ π₯ β 0β) β π΄ β
HAtoms)) |
45 | 44 | expdcom 413 |
. . . . 5
β’ (π₯ β β β (π₯ β 0β
β (π΄ =
(β₯β(β₯β{π₯})) β π΄ β HAtoms))) |
46 | 45 | impd 409 |
. . . 4
β’ (π₯ β β β ((π₯ β 0β β§
π΄ =
(β₯β(β₯β{π₯}))) β π΄ β HAtoms)) |
47 | 46 | rexlimiv 3146 |
. . 3
β’
(βπ₯ β
β (π₯ β
0β β§ π΄ = (β₯β(β₯β{π₯}))) β π΄ β HAtoms) |
48 | 41, 47 | impbii 208 |
. 2
β’ (π΄ β HAtoms β
βπ₯ β β
(π₯ β
0β β§ π΄ = (β₯β(β₯β{π₯})))) |
49 | | spansn 31077 |
. . . . 5
β’ (π₯ β β β
(spanβ{π₯}) =
(β₯β(β₯β{π₯}))) |
50 | 49 | eqeq2d 2741 |
. . . 4
β’ (π₯ β β β (π΄ = (spanβ{π₯}) β π΄ = (β₯β(β₯β{π₯})))) |
51 | 50 | anbi2d 627 |
. . 3
β’ (π₯ β β β ((π₯ β 0β β§
π΄ = (spanβ{π₯})) β (π₯ β 0β β§ π΄ =
(β₯β(β₯β{π₯}))))) |
52 | 51 | rexbiia 3090 |
. 2
β’
(βπ₯ β
β (π₯ β
0β β§ π΄ = (spanβ{π₯})) β βπ₯ β β (π₯ β 0β β§ π΄ =
(β₯β(β₯β{π₯})))) |
53 | 48, 52 | bitr4i 277 |
1
β’ (π΄ β HAtoms β
βπ₯ β β
(π₯ β
0β β§ π΄ = (spanβ{π₯}))) |