Step | Hyp | Ref
| Expression |
1 | | neibastop2.s |
. . . . 5
β’ π = {π¦ β π β£ βπ β βͺ ran
πΊ((πΉβπ¦) β© π« π) β β
} |
2 | | ssrab2 4038 |
. . . . 5
β’ {π¦ β π β£ βπ β βͺ ran
πΊ((πΉβπ¦) β© π« π) β β
} β π |
3 | 1, 2 | eqsstri 3979 |
. . . 4
β’ π β π |
4 | | neibastop1.1 |
. . . . 5
β’ (π β π β π) |
5 | | elpw2g 5302 |
. . . . 5
β’ (π β π β (π β π« π β π β π)) |
6 | 4, 5 | syl 17 |
. . . 4
β’ (π β (π β π« π β π β π)) |
7 | 3, 6 | mpbiri 258 |
. . 3
β’ (π β π β π« π) |
8 | | fveq2 6843 |
. . . . . . . . 9
β’ (π¦ = π₯ β (πΉβπ¦) = (πΉβπ₯)) |
9 | 8 | ineq1d 4172 |
. . . . . . . 8
β’ (π¦ = π₯ β ((πΉβπ¦) β© π« π) = ((πΉβπ₯) β© π« π)) |
10 | 9 | neeq1d 3000 |
. . . . . . 7
β’ (π¦ = π₯ β (((πΉβπ¦) β© π« π) β β
β ((πΉβπ₯) β© π« π) β β
)) |
11 | 10 | rexbidv 3172 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β βͺ ran
πΊ((πΉβπ¦) β© π« π) β β
β βπ β βͺ ran πΊ((πΉβπ₯) β© π« π) β β
)) |
12 | 11, 1 | elrab2 3649 |
. . . . 5
β’ (π₯ β π β (π₯ β π β§ βπ β βͺ ran
πΊ((πΉβπ₯) β© π« π) β β
)) |
13 | | frfnom 8382 |
. . . . . . . . . 10
β’
(rec((π β V
β¦ βͺ π§ β π βͺ π₯ β π ((πΉβπ₯) β© π« π§)), {π}) βΎ Ο) Fn
Ο |
14 | | neibastop2.g |
. . . . . . . . . . 11
β’ πΊ = (rec((π β V β¦ βͺ π§ β π βͺ π₯ β π ((πΉβπ₯) β© π« π§)), {π}) βΎ Ο) |
15 | 14 | fneq1i 6600 |
. . . . . . . . . 10
β’ (πΊ Fn Ο β (rec((π β V β¦ βͺ π§ β π βͺ π₯ β π ((πΉβπ₯) β© π« π§)), {π}) βΎ Ο) Fn
Ο) |
16 | 13, 15 | mpbir 230 |
. . . . . . . . 9
β’ πΊ Fn Ο |
17 | | fnunirn 7202 |
. . . . . . . . 9
β’ (πΊ Fn Ο β (π β βͺ ran πΊ β βπ β Ο π β (πΊβπ))) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . 8
β’ (π β βͺ ran πΊ β βπ β Ο π β (πΊβπ)) |
19 | | n0 4307 |
. . . . . . . . . 10
β’ (((πΉβπ₯) β© π« π) β β
β βπ£ π£ β ((πΉβπ₯) β© π« π)) |
20 | | inss1 4189 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ₯) β© π« π) β (πΉβπ₯) |
21 | 20 | sseli 3941 |
. . . . . . . . . . . . . . 15
β’ (π£ β ((πΉβπ₯) β© π« π) β π£ β (πΉβπ₯)) |
22 | | neibastop1.6 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β
) |
23 | 22 | anassrs 469 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π) β§ π£ β (πΉβπ₯)) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β
) |
24 | 21, 23 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π) β§ π£ β ((πΉβπ₯) β© π« π)) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β
) |
25 | 24 | adantrl 715 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β βπ‘ β (πΉβπ₯)βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β
) |
26 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ (π‘ β (πΉβπ₯) β§ βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β
)) β π‘ β (πΉβπ₯)) |
27 | | fvssunirn 6876 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΉβπ₯) β βͺ ran
πΉ |
28 | | neibastop1.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β πΉ:πβΆ(π« π« π β
{β
})) |
29 | 28 | frnd 6677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β ran πΉ β (π« π« π β
{β
})) |
30 | 29 | difss2d 4095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ran πΉ β π« π« π) |
31 | | sspwuni 5061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (ran
πΉ β π«
π« π β βͺ ran πΉ β π« π) |
32 | 30, 31 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β βͺ ran πΉ β π« π) |
33 | 32 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β βͺ ran
πΉ β π« π) |
34 | 27, 33 | sstrid 3956 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β (πΉβπ₯) β π« π) |
35 | 34 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ π‘ β (πΉβπ₯)) β π‘ β π« π) |
36 | 35 | elpwid 4570 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ π‘ β (πΉβπ₯)) β π‘ β π) |
37 | 36 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ π‘ β (πΉβπ₯)) β§ π¦ β π‘) β π¦ β π) |
38 | 37 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ π‘ β (πΉβπ₯)) β§ (π¦ β π‘ β§ ((πΉβπ¦) β© π« π£) β β
)) β π¦ β π) |
39 | | simprlr 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β π β (πΊβπ)) |
40 | | rspe 3231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π₯ β π β§ π£ β ((πΉβπ₯) β© π« π)) β βπ₯ β π π£ β ((πΉβπ₯) β© π« π)) |
41 | 40 | ad2ant2l 745 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β βπ₯ β π π£ β ((πΉβπ₯) β© π« π)) |
42 | | eliun 4959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π£ β βͺ π₯ β π ((πΉβπ₯) β© π« π§) β βπ₯ β π π£ β ((πΉβπ₯) β© π« π§)) |
43 | | pweq 4575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π§ = π β π« π§ = π« π) |
44 | 43 | ineq2d 4173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π§ = π β ((πΉβπ₯) β© π« π§) = ((πΉβπ₯) β© π« π)) |
45 | 44 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π§ = π β (π£ β ((πΉβπ₯) β© π« π§) β π£ β ((πΉβπ₯) β© π« π))) |
46 | 45 | rexbidv 3172 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π§ = π β (βπ₯ β π π£ β ((πΉβπ₯) β© π« π§) β βπ₯ β π π£ β ((πΉβπ₯) β© π« π))) |
47 | 42, 46 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ = π β (π£ β βͺ
π₯ β π ((πΉβπ₯) β© π« π§) β βπ₯ β π π£ β ((πΉβπ₯) β© π« π))) |
48 | 47 | rspcev 3580 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (πΊβπ) β§ βπ₯ β π π£ β ((πΉβπ₯) β© π« π)) β βπ§ β (πΊβπ)π£ β βͺ
π₯ β π ((πΉβπ₯) β© π« π§)) |
49 | 39, 41, 48 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β βπ§ β (πΊβπ)π£ β βͺ
π₯ β π ((πΉβπ₯) β© π« π§)) |
50 | | eliun 4959 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π£ β βͺ π§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§) β βπ§ β (πΊβπ)π£ β βͺ
π₯ β π ((πΉβπ₯) β© π« π§)) |
51 | 49, 50 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β π£ β βͺ
π§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§)) |
52 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β π) |
53 | | simprll 778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β π β Ο) |
54 | | fvssunirn 6876 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πΊβπ) β βͺ ran
πΊ |
55 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π = β
β (πΊβπ) = (πΊββ
)) |
56 | 14 | fveq1i 6844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (πΊββ
) = ((rec((π β V β¦ βͺ π§ β π βͺ π₯ β π ((πΉβπ₯) β© π« π§)), {π}) βΎ
Ο)ββ
) |
57 | | snex 5389 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ {π} β V |
58 | | fr0g 8383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ({π} β V β ((rec((π β V β¦ βͺ π§ β π βͺ π₯ β π ((πΉβπ₯) β© π« π§)), {π}) βΎ Ο)ββ
) = {π}) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((rec((π β V
β¦ βͺ π§ β π βͺ π₯ β π ((πΉβπ₯) β© π« π§)), {π}) βΎ Ο)ββ
) = {π} |
60 | 56, 59 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (πΊββ
) = {π} |
61 | 55, 60 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = β
β (πΊβπ) = {π}) |
62 | 61 | sseq1d 3976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = β
β ((πΊβπ) β π« π β {π} β π« π)) |
63 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π β (πΊβπ) = (πΊβπ)) |
64 | 63 | sseq1d 3976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π β ((πΊβπ) β π« π β (πΊβπ) β π« π)) |
65 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = suc π β (πΊβπ) = (πΊβsuc π)) |
66 | 65 | sseq1d 3976 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = suc π β ((πΊβπ) β π« π β (πΊβsuc π) β π« π)) |
67 | | neibastop2.f |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β π β (πΉβπ)) |
68 | | pwidg 4581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β (πΉβπ) β π β π« π) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β π β π« π) |
70 | 69 | snssd 4770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β {π} β π« π) |
71 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β§ (π β Ο β§ (πΊβπ) β π« π)) β π β Ο) |
72 | 67 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π β§ (π β Ο β§ (πΊβπ) β π« π)) β π β (πΉβπ)) |
73 | 72 | pwexd 5335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β§ (π β Ο β§ (πΊβπ) β π« π)) β π« π β V) |
74 | | inss2 4190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((πΉβπ₯) β© π« π§) β π« π§ |
75 | | elpwi 4568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’ (π§ β π« π β π§ β π) |
76 | 75 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ ((π β§ π§ β π« π) β π§ β π) |
77 | 76 | sspwd 4574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ ((π β§ π§ β π« π) β π« π§ β π« π) |
78 | 74, 77 | sstrid 3956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ ((π β§ π§ β π« π) β ((πΉβπ₯) β© π« π§) β π« π) |
79 | 78 | ralrimivw 3144 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((π β§ π§ β π« π) β βπ₯ β π ((πΉβπ₯) β© π« π§) β π« π) |
80 | | iunss 5006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (βͺ π₯ β π ((πΉβπ₯) β© π« π§) β π« π β βπ₯ β π ((πΉβπ₯) β© π« π§) β π« π) |
81 | 79, 80 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((π β§ π§ β π« π) β βͺ
π₯ β π ((πΉβπ₯) β© π« π§) β π« π) |
82 | 81 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (π β βπ§ β π« πβͺ π₯ β π ((πΉβπ₯) β© π« π§) β π« π) |
83 | | ssralv 4011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((πΊβπ) β π« π β (βπ§ β π« πβͺ π₯ β π ((πΉβπ₯) β© π« π§) β π« π β βπ§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§) β π« π)) |
84 | 83 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((π β Ο β§ (πΊβπ) β π« π) β (βπ§ β π« πβͺ π₯ β π ((πΉβπ₯) β© π« π§) β π« π β βπ§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§) β π« π)) |
85 | 82, 84 | mpan9 508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π β§ (π β Ο β§ (πΊβπ) β π« π)) β βπ§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§) β π« π) |
86 | | iunss 5006 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (βͺ π§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§) β π« π β βπ§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§) β π« π) |
87 | 85, 86 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β§ (π β Ο β§ (πΊβπ) β π« π)) β βͺ π§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§) β π« π) |
88 | 73, 87 | ssexd 5282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β§ (π β Ο β§ (πΊβπ) β π« π)) β βͺ π§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§) β V) |
89 | | iuneq1 4971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π¦ = π β βͺ
π§ β π¦ βͺ π₯ β π ((πΉβπ₯) β© π« π§) = βͺ π§ β π βͺ π₯ β π ((πΉβπ₯) β© π« π§)) |
90 | | iuneq1 4971 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π¦ = (πΊβπ) β βͺ
π§ β π¦ βͺ π₯ β π ((πΉβπ₯) β© π« π§) = βͺ π§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§)) |
91 | 14, 89, 90 | frsucmpt2 8387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β Ο β§ βͺ π§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§) β V) β (πΊβsuc π) = βͺ π§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§)) |
92 | 71, 88, 91 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β§ (π β Ο β§ (πΊβπ) β π« π)) β (πΊβsuc π) = βͺ π§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§)) |
93 | 92, 87 | eqsstrd 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β§ (π β Ο β§ (πΊβπ) β π« π)) β (πΊβsuc π) β π« π) |
94 | 93 | expr 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β§ π β Ο) β ((πΊβπ) β π« π β (πΊβsuc π) β π« π)) |
95 | 94 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β Ο β (π β ((πΊβπ) β π« π β (πΊβsuc π) β π« π))) |
96 | 62, 64, 66, 70, 95 | finds2 7838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β Ο β (π β (πΊβπ) β π« π)) |
97 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (πΊβπ) β V |
98 | 97 | elpw 4565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((πΊβπ) β π« π« π β (πΊβπ) β π« π) |
99 | 96, 98 | syl6ibr 252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β Ο β (π β (πΊβπ) β π« π« π)) |
100 | 99 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (π β Ο β (πΊβπ) β π« π« π)) |
101 | 100 | ralrimiv 3139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β βπ β Ο (πΊβπ) β π« π« π) |
102 | | ffnfv 7067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (πΊ:ΟβΆπ«
π« π β (πΊ Fn Ο β§ βπ β Ο (πΊβπ) β π« π« π)) |
103 | 16, 102 | mpbiran 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (πΊ:ΟβΆπ«
π« π β
βπ β Ο
(πΊβπ) β π« π« π) |
104 | 101, 103 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β πΊ:ΟβΆπ« π« π) |
105 | 104 | frnd 6677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β ran πΊ β π« π« π) |
106 | | sspwuni 5061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (ran
πΊ β π«
π« π β βͺ ran πΊ β π« π) |
107 | 105, 106 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β βͺ ran πΊ β π« π) |
108 | 107 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β βͺ ran
πΊ β π« π) |
109 | 54, 108 | sstrid 3956 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β (πΊβπ) β π« π) |
110 | 52, 53, 109, 92 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β (πΊβsuc π) = βͺ π§ β (πΊβπ)βͺ π₯ β π ((πΉβπ₯) β© π« π§)) |
111 | 51, 110 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β π£ β (πΊβsuc π)) |
112 | | peano2 7828 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β Ο β suc π β
Ο) |
113 | 53, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β suc π β Ο) |
114 | | fnfvelrn 7032 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πΊ Fn Ο β§ suc π β Ο) β (πΊβsuc π) β ran πΊ) |
115 | 16, 113, 114 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β (πΊβsuc π) β ran πΊ) |
116 | | elunii 4871 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π£ β (πΊβsuc π) β§ (πΊβsuc π) β ran πΊ) β π£ β βͺ ran
πΊ) |
117 | 111, 115,
116 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β π£ β βͺ ran
πΊ) |
118 | 117 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ π‘ β (πΉβπ₯)) β§ (π¦ β π‘ β§ ((πΉβπ¦) β© π« π£) β β
)) β π£ β βͺ ran
πΊ) |
119 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ π‘ β (πΉβπ₯)) β§ (π¦ β π‘ β§ ((πΉβπ¦) β© π« π£) β β
)) β ((πΉβπ¦) β© π« π£) β β
) |
120 | | pweq 4575 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = π£ β π« π = π« π£) |
121 | 120 | ineq2d 4173 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π£ β ((πΉβπ¦) β© π« π) = ((πΉβπ¦) β© π« π£)) |
122 | 121 | neeq1d 3000 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π£ β (((πΉβπ¦) β© π« π) β β
β ((πΉβπ¦) β© π« π£) β β
)) |
123 | 122 | rspcev 3580 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π£ β βͺ ran πΊ β§ ((πΉβπ¦) β© π« π£) β β
) β βπ β βͺ ran πΊ((πΉβπ¦) β© π« π) β β
) |
124 | 118, 119,
123 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ π‘ β (πΉβπ₯)) β§ (π¦ β π‘ β§ ((πΉβπ¦) β© π« π£) β β
)) β βπ β βͺ ran πΊ((πΉβπ¦) β© π« π) β β
) |
125 | 1 | reqabi 3428 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β π β (π¦ β π β§ βπ β βͺ ran
πΊ((πΉβπ¦) β© π« π) β β
)) |
126 | 38, 124, 125 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ π‘ β (πΉβπ₯)) β§ (π¦ β π‘ β§ ((πΉβπ¦) β© π« π£) β β
)) β π¦ β π) |
127 | 126 | expr 458 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ π‘ β (πΉβπ₯)) β§ π¦ β π‘) β (((πΉβπ¦) β© π« π£) β β
β π¦ β π)) |
128 | 127 | ralimdva 3161 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ π‘ β (πΉβπ₯)) β (βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β
β βπ¦ β π‘ π¦ β π)) |
129 | 128 | impr 456 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ (π‘ β (πΉβπ₯) β§ βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β
)) β βπ¦ β π‘ π¦ β π) |
130 | | dfss3 3933 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β π β βπ¦ β π‘ π¦ β π) |
131 | 129, 130 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ (π‘ β (πΉβπ₯) β§ βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β
)) β π‘ β π) |
132 | | velpw 4566 |
. . . . . . . . . . . . . . 15
β’ (π‘ β π« π β π‘ β π) |
133 | 131, 132 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ (π‘ β (πΉβπ₯) β§ βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β
)) β π‘ β π« π) |
134 | | inelcm 4425 |
. . . . . . . . . . . . . 14
β’ ((π‘ β (πΉβπ₯) β§ π‘ β π« π) β ((πΉβπ₯) β© π« π) β β
) |
135 | 26, 133, 134 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β§ (π‘ β (πΉβπ₯) β§ βπ¦ β π‘ ((πΉβπ¦) β© π« π£) β β
)) β ((πΉβπ₯) β© π« π) β β
) |
136 | 25, 135 | rexlimddv 3155 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π) β§ ((π β Ο β§ π β (πΊβπ)) β§ π£ β ((πΉβπ₯) β© π« π))) β ((πΉβπ₯) β© π« π) β β
) |
137 | 136 | expr 458 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π) β§ (π β Ο β§ π β (πΊβπ))) β (π£ β ((πΉβπ₯) β© π« π) β ((πΉβπ₯) β© π« π) β β
)) |
138 | 137 | exlimdv 1937 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π) β§ (π β Ο β§ π β (πΊβπ))) β (βπ£ π£ β ((πΉβπ₯) β© π« π) β ((πΉβπ₯) β© π« π) β β
)) |
139 | 19, 138 | biimtrid 241 |
. . . . . . . . 9
β’ (((π β§ π₯ β π) β§ (π β Ο β§ π β (πΊβπ))) β (((πΉβπ₯) β© π« π) β β
β ((πΉβπ₯) β© π« π) β β
)) |
140 | 139 | rexlimdvaa 3150 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (βπ β Ο π β (πΊβπ) β (((πΉβπ₯) β© π« π) β β
β ((πΉβπ₯) β© π« π) β β
))) |
141 | 18, 140 | biimtrid 241 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (π β βͺ ran
πΊ β (((πΉβπ₯) β© π« π) β β
β ((πΉβπ₯) β© π« π) β β
))) |
142 | 141 | rexlimdv 3147 |
. . . . . 6
β’ ((π β§ π₯ β π) β (βπ β βͺ ran
πΊ((πΉβπ₯) β© π« π) β β
β ((πΉβπ₯) β© π« π) β β
)) |
143 | 142 | expimpd 455 |
. . . . 5
β’ (π β ((π₯ β π β§ βπ β βͺ ran
πΊ((πΉβπ₯) β© π« π) β β
) β ((πΉβπ₯) β© π« π) β β
)) |
144 | 12, 143 | biimtrid 241 |
. . . 4
β’ (π β (π₯ β π β ((πΉβπ₯) β© π« π) β β
)) |
145 | 144 | ralrimiv 3139 |
. . 3
β’ (π β βπ₯ β π ((πΉβπ₯) β© π« π) β β
) |
146 | | pweq 4575 |
. . . . . . 7
β’ (π = π β π« π = π« π) |
147 | 146 | ineq2d 4173 |
. . . . . 6
β’ (π = π β ((πΉβπ₯) β© π« π) = ((πΉβπ₯) β© π« π)) |
148 | 147 | neeq1d 3000 |
. . . . 5
β’ (π = π β (((πΉβπ₯) β© π« π) β β
β ((πΉβπ₯) β© π« π) β β
)) |
149 | 148 | raleqbi1dv 3306 |
. . . 4
β’ (π = π β (βπ₯ β π ((πΉβπ₯) β© π« π) β β
β βπ₯ β π ((πΉβπ₯) β© π« π) β β
)) |
150 | | neibastop1.4 |
. . . 4
β’ π½ = {π β π« π β£ βπ₯ β π ((πΉβπ₯) β© π« π) β β
} |
151 | 149, 150 | elrab2 3649 |
. . 3
β’ (π β π½ β (π β π« π β§ βπ₯ β π ((πΉβπ₯) β© π« π) β β
)) |
152 | 7, 145, 151 | sylanbrc 584 |
. 2
β’ (π β π β π½) |
153 | | neibastop2.p |
. . 3
β’ (π β π β π) |
154 | | snidg 4621 |
. . . . . 6
β’ (π β (πΉβπ) β π β {π}) |
155 | 67, 154 | syl 17 |
. . . . 5
β’ (π β π β {π}) |
156 | | peano1 7826 |
. . . . . . 7
β’ β
β Ο |
157 | | fnfvelrn 7032 |
. . . . . . 7
β’ ((πΊ Fn Ο β§ β
β
Ο) β (πΊββ
) β ran πΊ) |
158 | 16, 156, 157 | mp2an 691 |
. . . . . 6
β’ (πΊββ
) β ran πΊ |
159 | 60, 158 | eqeltrri 2831 |
. . . . 5
β’ {π} β ran πΊ |
160 | | elunii 4871 |
. . . . 5
β’ ((π β {π} β§ {π} β ran πΊ) β π β βͺ ran
πΊ) |
161 | 155, 159,
160 | sylancl 587 |
. . . 4
β’ (π β π β βͺ ran
πΊ) |
162 | | inelcm 4425 |
. . . . 5
β’ ((π β (πΉβπ) β§ π β π« π) β ((πΉβπ) β© π« π) β β
) |
163 | 67, 69, 162 | syl2anc 585 |
. . . 4
β’ (π β ((πΉβπ) β© π« π) β β
) |
164 | | pweq 4575 |
. . . . . . 7
β’ (π = π β π« π = π« π) |
165 | 164 | ineq2d 4173 |
. . . . . 6
β’ (π = π β ((πΉβπ) β© π« π) = ((πΉβπ) β© π« π)) |
166 | 165 | neeq1d 3000 |
. . . . 5
β’ (π = π β (((πΉβπ) β© π« π) β β
β ((πΉβπ) β© π« π) β β
)) |
167 | 166 | rspcev 3580 |
. . . 4
β’ ((π β βͺ ran πΊ β§ ((πΉβπ) β© π« π) β β
) β βπ β βͺ ran πΊ((πΉβπ) β© π« π) β β
) |
168 | 161, 163,
167 | syl2anc 585 |
. . 3
β’ (π β βπ β βͺ ran
πΊ((πΉβπ) β© π« π) β β
) |
169 | | fveq2 6843 |
. . . . . . 7
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
170 | 169 | ineq1d 4172 |
. . . . . 6
β’ (π¦ = π β ((πΉβπ¦) β© π« π) = ((πΉβπ) β© π« π)) |
171 | 170 | neeq1d 3000 |
. . . . 5
β’ (π¦ = π β (((πΉβπ¦) β© π« π) β β
β ((πΉβπ) β© π« π) β β
)) |
172 | 171 | rexbidv 3172 |
. . . 4
β’ (π¦ = π β (βπ β βͺ ran
πΊ((πΉβπ¦) β© π« π) β β
β βπ β βͺ ran πΊ((πΉβπ) β© π« π) β β
)) |
173 | 172, 1 | elrab2 3649 |
. . 3
β’ (π β π β (π β π β§ βπ β βͺ ran
πΊ((πΉβπ) β© π« π) β β
)) |
174 | 153, 168,
173 | sylanbrc 584 |
. 2
β’ (π β π β π) |
175 | | eluni2 4870 |
. . . . . . 7
β’ (π β βͺ ran πΊ β βπ§ β ran πΊ π β π§) |
176 | | eleq2 2823 |
. . . . . . . . . 10
β’ (π§ = (πΊβπ) β (π β π§ β π β (πΊβπ))) |
177 | 176 | rexrn 7038 |
. . . . . . . . 9
β’ (πΊ Fn Ο β (βπ§ β ran πΊ π β π§ β βπ β Ο π β (πΊβπ))) |
178 | 16, 177 | ax-mp 5 |
. . . . . . . 8
β’
(βπ§ β ran
πΊ π β π§ β βπ β Ο π β (πΊβπ)) |
179 | 104 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π¦ β π) β πΊ:ΟβΆπ« π« π) |
180 | 179 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β π) β§ π β Ο) β (πΊβπ) β π« π« π) |
181 | 180 | elpwid 4570 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β π) β§ π β Ο) β (πΊβπ) β π« π) |
182 | 181 | sselda 3945 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ π β (πΊβπ)) β π β π« π) |
183 | 182 | adantrr 716 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ ((πΉβπ¦) β© π« π) β β
)) β π β π« π) |
184 | 183 | elpwid 4570 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ ((πΉβπ¦) β© π« π) β β
)) β π β π) |
185 | | neibastop2.u |
. . . . . . . . . . . . 13
β’ (π β π β π) |
186 | 185 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ ((πΉβπ¦) β© π« π) β β
)) β π β π) |
187 | 184, 186 | sstrd 3955 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ ((πΉβπ¦) β© π« π) β β
)) β π β π) |
188 | | n0 4307 |
. . . . . . . . . . . . 13
β’ (((πΉβπ¦) β© π« π) β β
β βπ£ π£ β ((πΉβπ¦) β© π« π)) |
189 | | elin 3927 |
. . . . . . . . . . . . . . 15
β’ (π£ β ((πΉβπ¦) β© π« π) β (π£ β (πΉβπ¦) β§ π£ β π« π)) |
190 | | simprrr 781 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ (π£ β (πΉβπ¦) β§ π£ β π« π))) β π£ β π« π) |
191 | 190 | elpwid 4570 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ (π£ β (πΉβπ¦) β§ π£ β π« π))) β π£ β π) |
192 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ (π£ β (πΉβπ¦) β§ π£ β π« π))) β π¦ β π) |
193 | | neibastop1.5 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ (π₯ β π β§ π£ β (πΉβπ₯))) β π₯ β π£) |
194 | 193 | expr 458 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β π) β (π£ β (πΉβπ₯) β π₯ β π£)) |
195 | 194 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β βπ₯ β π (π£ β (πΉβπ₯) β π₯ β π£)) |
196 | 195 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ (π£ β (πΉβπ¦) β§ π£ β π« π))) β βπ₯ β π (π£ β (πΉβπ₯) β π₯ β π£)) |
197 | | simprrl 780 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ (π£ β (πΉβπ¦) β§ π£ β π« π))) β π£ β (πΉβπ¦)) |
198 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π¦ β (πΉβπ₯) = (πΉβπ¦)) |
199 | 198 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π¦ β (π£ β (πΉβπ₯) β π£ β (πΉβπ¦))) |
200 | | elequ1 2114 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ = π¦ β (π₯ β π£ β π¦ β π£)) |
201 | 199, 200 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ = π¦ β ((π£ β (πΉβπ₯) β π₯ β π£) β (π£ β (πΉβπ¦) β π¦ β π£))) |
202 | 201 | rspcv 3576 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β π β (βπ₯ β π (π£ β (πΉβπ₯) β π₯ β π£) β (π£ β (πΉβπ¦) β π¦ β π£))) |
203 | 192, 196,
197, 202 | syl3c 66 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ (π£ β (πΉβπ¦) β§ π£ β π« π))) β π¦ β π£) |
204 | 191, 203 | sseldd 3946 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ (π£ β (πΉβπ¦) β§ π£ β π« π))) β π¦ β π) |
205 | 204 | expr 458 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ π β (πΊβπ)) β ((π£ β (πΉβπ¦) β§ π£ β π« π) β π¦ β π)) |
206 | 189, 205 | biimtrid 241 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ π β (πΊβπ)) β (π£ β ((πΉβπ¦) β© π« π) β π¦ β π)) |
207 | 206 | exlimdv 1937 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ π β (πΊβπ)) β (βπ£ π£ β ((πΉβπ¦) β© π« π) β π¦ β π)) |
208 | 188, 207 | biimtrid 241 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ π β (πΊβπ)) β (((πΉβπ¦) β© π« π) β β
β π¦ β π)) |
209 | 208 | impr 456 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ ((πΉβπ¦) β© π« π) β β
)) β π¦ β π) |
210 | 187, 209 | sseldd 3946 |
. . . . . . . . . 10
β’ ((((π β§ π¦ β π) β§ π β Ο) β§ (π β (πΊβπ) β§ ((πΉβπ¦) β© π« π) β β
)) β π¦ β π) |
211 | 210 | exp32 422 |
. . . . . . . . 9
β’ (((π β§ π¦ β π) β§ π β Ο) β (π β (πΊβπ) β (((πΉβπ¦) β© π« π) β β
β π¦ β π))) |
212 | 211 | rexlimdva 3149 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (βπ β Ο π β (πΊβπ) β (((πΉβπ¦) β© π« π) β β
β π¦ β π))) |
213 | 178, 212 | biimtrid 241 |
. . . . . . 7
β’ ((π β§ π¦ β π) β (βπ§ β ran πΊ π β π§ β (((πΉβπ¦) β© π« π) β β
β π¦ β π))) |
214 | 175, 213 | biimtrid 241 |
. . . . . 6
β’ ((π β§ π¦ β π) β (π β βͺ ran
πΊ β (((πΉβπ¦) β© π« π) β β
β π¦ β π))) |
215 | 214 | rexlimdv 3147 |
. . . . 5
β’ ((π β§ π¦ β π) β (βπ β βͺ ran
πΊ((πΉβπ¦) β© π« π) β β
β π¦ β π)) |
216 | 215 | 3impia 1118 |
. . . 4
β’ ((π β§ π¦ β π β§ βπ β βͺ ran
πΊ((πΉβπ¦) β© π« π) β β
) β π¦ β π) |
217 | 216 | rabssdv 4033 |
. . 3
β’ (π β {π¦ β π β£ βπ β βͺ ran
πΊ((πΉβπ¦) β© π« π) β β
} β π) |
218 | 1, 217 | eqsstrid 3993 |
. 2
β’ (π β π β π) |
219 | | eleq2 2823 |
. . . 4
β’ (π’ = π β (π β π’ β π β π)) |
220 | | sseq1 3970 |
. . . 4
β’ (π’ = π β (π’ β π β π β π)) |
221 | 219, 220 | anbi12d 632 |
. . 3
β’ (π’ = π β ((π β π’ β§ π’ β π) β (π β π β§ π β π))) |
222 | 221 | rspcev 3580 |
. 2
β’ ((π β π½ β§ (π β π β§ π β π)) β βπ’ β π½ (π β π’ β§ π’ β π)) |
223 | 152, 174,
218, 222 | syl12anc 836 |
1
β’ (π β βπ’ β π½ (π β π’ β§ π’ β π)) |