Step | Hyp | Ref
| Expression |
1 | | nfe1 2148 |
. . . . 5
β’
β²π₯βπ₯(π₯ β π β§ π) |
2 | | nfcv 2908 |
. . . . 5
β’
β²π₯Ο |
3 | 1, 2 | nfrabw 3443 |
. . . 4
β’
β²π₯{π β Ο β£ βπ₯(π₯ β π β§ π)} |
4 | | nfcv 2908 |
. . . 4
β’
β²π₯β
|
5 | 3, 4 | nfne 3046 |
. . 3
β’
β²π₯{π β Ο β£
βπ₯(π₯ β π β§ π)} β β
|
6 | | isfi 8923 |
. . . 4
β’ (π₯ β Fin β βπ β Ο π₯ β π) |
7 | | 19.8a 2175 |
. . . . . . . . . 10
β’ ((π₯ β π β§ π) β βπ₯(π₯ β π β§ π)) |
8 | 7 | anim2i 618 |
. . . . . . . . 9
β’ ((π β Ο β§ (π₯ β π β§ π)) β (π β Ο β§ βπ₯(π₯ β π β§ π))) |
9 | 8 | 3impb 1116 |
. . . . . . . 8
β’ ((π β Ο β§ π₯ β π β§ π) β (π β Ο β§ βπ₯(π₯ β π β§ π))) |
10 | | breq2 5114 |
. . . . . . . . . . 11
β’ (π = π β (π₯ β π β π₯ β π)) |
11 | 10 | anbi1d 631 |
. . . . . . . . . 10
β’ (π = π β ((π₯ β π β§ π) β (π₯ β π β§ π))) |
12 | 11 | exbidv 1925 |
. . . . . . . . 9
β’ (π = π β (βπ₯(π₯ β π β§ π) β βπ₯(π₯ β π β§ π))) |
13 | 12 | elrab 3650 |
. . . . . . . 8
β’ (π β {π β Ο β£ βπ₯(π₯ β π β§ π)} β (π β Ο β§ βπ₯(π₯ β π β§ π))) |
14 | 9, 13 | sylibr 233 |
. . . . . . 7
β’ ((π β Ο β§ π₯ β π β§ π) β π β {π β Ο β£ βπ₯(π₯ β π β§ π)}) |
15 | 14 | ne0d 4300 |
. . . . . 6
β’ ((π β Ο β§ π₯ β π β§ π) β {π β Ο β£ βπ₯(π₯ β π β§ π)} β β
) |
16 | 15 | 3exp 1120 |
. . . . 5
β’ (π β Ο β (π₯ β π β (π β {π β Ο β£ βπ₯(π₯ β π β§ π)} β β
))) |
17 | 16 | rexlimiv 3146 |
. . . 4
β’
(βπ β
Ο π₯ β π β (π β {π β Ο β£ βπ₯(π₯ β π β§ π)} β β
)) |
18 | 6, 17 | sylbi 216 |
. . 3
β’ (π₯ β Fin β (π β {π β Ο β£ βπ₯(π₯ β π β§ π)} β β
)) |
19 | 5, 18 | rexlimi 3245 |
. 2
β’
(βπ₯ β Fin
π β {π β Ο β£ βπ₯(π₯ β π β§ π)} β β
) |
20 | | epweon 7714 |
. . 3
β’ E We
On |
21 | | ssrab2 4042 |
. . . 4
β’ {π β Ο β£
βπ₯(π₯ β π β§ π)} β Ο |
22 | | omsson 7811 |
. . . 4
β’ Ο
β On |
23 | 21, 22 | sstri 3958 |
. . 3
β’ {π β Ο β£
βπ₯(π₯ β π β§ π)} β On |
24 | | wefrc 5632 |
. . 3
β’ (( E We
On β§ {π β Ο
β£ βπ₯(π₯ β π β§ π)} β On β§ {π β Ο β£ βπ₯(π₯ β π β§ π)} β β
) β βπ β {π β Ο β£ βπ₯(π₯ β π β§ π)} ({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) = β
) |
25 | 20, 23, 24 | mp3an12 1452 |
. 2
β’ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β β
β βπ β {π β Ο β£ βπ₯(π₯ β π β§ π)} ({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) = β
) |
26 | | nfv 1918 |
. . . . . . 7
β’
β²π₯ π β Ο |
27 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π₯π |
28 | 3, 27 | nfin 4181 |
. . . . . . . 8
β’
β²π₯({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) |
29 | 28 | nfeq1 2923 |
. . . . . . 7
β’
β²π₯({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
|
30 | 26, 29 | nfan 1903 |
. . . . . 6
β’
β²π₯(π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) |
31 | | simprr 772 |
. . . . . . . 8
β’ (((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β§ (π₯ β π β§ π)) β π) |
32 | | sspss 4064 |
. . . . . . . . . . . . 13
β’ (π¦ β π₯ β (π¦ β π₯ β¨ π¦ = π₯)) |
33 | | rspe 3235 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Ο β§ π₯ β π) β βπ β Ο π₯ β π) |
34 | | pssss 4060 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β π₯ β π¦ β π₯) |
35 | | ssfi 9124 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π₯ β Fin β§ π¦ β π₯) β π¦ β Fin) |
36 | 34, 35 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π₯ β Fin β§ π¦ β π₯) β π¦ β Fin) |
37 | 36 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π₯ β Fin β (π¦ β π₯ β π¦ β Fin)) |
38 | 6, 37 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(βπ β
Ο π₯ β π β (π¦ β π₯ β π¦ β Fin)) |
39 | 33, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Ο β§ π₯ β π) β (π¦ β π₯ β π¦ β Fin)) |
40 | 39 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β Ο β§ (π₯ β π β§ π)) β (π¦ β π₯ β π¦ β Fin)) |
41 | 40 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Ο β§ ((π₯ β π β§ π) β§ π)) β (π¦ β π₯ β π¦ β Fin)) |
42 | | isfi 8923 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π¦ β Fin β βπ β Ο π¦ β π) |
43 | | simprll 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ ((π β Ο β§ π¦ β π) β§ π¦ β π₯)) β π β Ο) |
44 | | simprlr 779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ ((π β Ο β§ π¦ β π) β§ π¦ β π₯)) β π¦ β π) |
45 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ ((π β Ο β§ π¦ β π) β§ π¦ β π₯)) β π) |
46 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ π¦ β V |
47 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π₯ = π¦ β (π₯ β π β π¦ β π)) |
48 | | finminlem.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π₯ = π¦ β (π β π)) |
49 | 47, 48 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π₯ = π¦ β ((π₯ β π β§ π) β (π¦ β π β§ π))) |
50 | 46, 49 | spcev 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π¦ β π β§ π) β βπ₯(π₯ β π β§ π)) |
51 | 44, 45, 50 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ ((π β Ο β§ π¦ β π) β§ π¦ β π₯)) β βπ₯(π₯ β π β§ π)) |
52 | 33, 6 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β Ο β§ π₯ β π) β π₯ β Fin) |
53 | 52 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β Ο β§ (π₯ β π β§ π)) β π₯ β Fin) |
54 | 53 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β Ο β§ ((π₯ β π β§ π) β§ π)) β π₯ β Fin) |
55 | 54 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ (π β Ο β§ π¦ β π)) β π₯ β Fin) |
56 | | php3 9163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π₯ β Fin β§ π¦ β π₯) β π¦ βΊ π₯) |
57 | 56 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π₯ β Fin β (π¦ β π₯ β π¦ βΊ π₯)) |
58 | 55, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ (π β Ο β§ π¦ β π)) β (π¦ β π₯ β π¦ βΊ π₯)) |
59 | | vex 3452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ π β V |
60 | | ssdomg 8947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β V β (π β π β π βΌ π)) |
61 | 59, 60 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β π β π βΌ π) |
62 | | endomtr 8959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π₯ β π β§ π βΌ π) β π₯ βΌ π) |
63 | 62 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π₯ β π β (π βΌ π β π₯ βΌ π)) |
64 | 63 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π₯ β π β§ π) β§ π) β (π βΌ π β π₯ βΌ π)) |
65 | 64 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ (π β Ο β§ π¦ β π)) β (π βΌ π β π₯ βΌ π)) |
66 | | ensym 8950 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π¦ β π β π β π¦) |
67 | | domentr 8960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π₯ βΌ π β§ π β π¦) β π₯ βΌ π¦) |
68 | 66, 67 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π₯ βΌ π β§ π¦ β π) β π₯ βΌ π¦) |
69 | 68 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π¦ β π β (π₯ βΌ π β π₯ βΌ π¦)) |
70 | 69 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ (π β Ο β§ π¦ β π)) β (π₯ βΌ π β π₯ βΌ π¦)) |
71 | 65, 70 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ (π β Ο β§ π¦ β π)) β (π βΌ π β π₯ βΌ π¦)) |
72 | 61, 71 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ (π β Ο β§ π¦ β π)) β (π β π β π₯ βΌ π¦)) |
73 | | domnsym 9050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π₯ βΌ π¦ β Β¬ π¦ βΊ π₯) |
74 | 73 | con2i 139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π¦ βΊ π₯ β Β¬ π₯ βΌ π¦) |
75 | 72, 74 | nsyli 157 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ (π β Ο β§ π¦ β π)) β (π¦ βΊ π₯ β Β¬ π β π)) |
76 | 58, 75 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ (π β Ο β§ π¦ β π)) β (π¦ β π₯ β Β¬ π β π)) |
77 | 76 | impr 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ ((π β Ο β§ π¦ β π) β§ π¦ β π₯)) β Β¬ π β π) |
78 | | nnord 7815 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β Ο β Ord π) |
79 | 78 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ ((π β Ο β§ π¦ β π) β§ π¦ β π₯)) β Ord π) |
80 | | nnord 7815 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β Ο β Ord π) |
81 | 80 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β Ο β§ π¦ β π) β Ord π) |
82 | 81 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ ((π β Ο β§ π¦ β π) β§ π¦ β π₯)) β Ord π) |
83 | | ordtri1 6355 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((Ord
π β§ Ord π) β (π β π β Β¬ π β π)) |
84 | 83 | con2bid 355 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((Ord
π β§ Ord π) β (π β π β Β¬ π β π)) |
85 | 79, 82, 84 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ ((π β Ο β§ π¦ β π) β§ π¦ β π₯)) β (π β π β Β¬ π β π)) |
86 | 77, 85 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ ((π β Ο β§ π¦ β π) β§ π¦ β π₯)) β π β π) |
87 | 43, 51, 86 | jca31 516 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ ((π β Ο β§ π¦ β π) β§ π¦ β π₯)) β ((π β Ο β§ βπ₯(π₯ β π β§ π)) β§ π β π)) |
88 | | elin 3931 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β ({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) β (π β {π β Ο β£ βπ₯(π₯ β π β§ π)} β§ π β π)) |
89 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = π β (π₯ β π β π₯ β π)) |
90 | 89 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β ((π₯ β π β§ π) β (π₯ β π β§ π))) |
91 | 90 | exbidv 1925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π β (βπ₯(π₯ β π β§ π) β βπ₯(π₯ β π β§ π))) |
92 | 91 | elrab 3650 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β {π β Ο β£ βπ₯(π₯ β π β§ π)} β (π β Ο β§ βπ₯(π₯ β π β§ π))) |
93 | 92 | anbi1i 625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β {π β Ο β£ βπ₯(π₯ β π β§ π)} β§ π β π) β ((π β Ο β§ βπ₯(π₯ β π β§ π)) β§ π β π)) |
94 | 88, 93 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β ({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) β ((π β Ο β§ βπ₯(π₯ β π β§ π)) β§ π β π)) |
95 | 87, 94 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ ((π β Ο β§ π¦ β π) β§ π¦ β π₯)) β π β ({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π)) |
96 | 95 | ne0d 4300 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β Ο β§ ((π₯ β π β§ π) β§ π)) β§ ((π β Ο β§ π¦ β π) β§ π¦ β π₯)) β ({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) β β
) |
97 | 96 | exp44 439 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Ο β§ ((π₯ β π β§ π) β§ π)) β (π β Ο β (π¦ β π β (π¦ β π₯ β ({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) β β
)))) |
98 | 97 | rexlimdv 3151 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Ο β§ ((π₯ β π β§ π) β§ π)) β (βπ β Ο π¦ β π β (π¦ β π₯ β ({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) β β
))) |
99 | 42, 98 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β Ο β§ ((π₯ β π β§ π) β§ π)) β (π¦ β Fin β (π¦ β π₯ β ({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) β β
))) |
100 | 99 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β Ο β§ ((π₯ β π β§ π) β§ π)) β (π¦ β π₯ β (π¦ β Fin β ({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) β β
))) |
101 | 41, 100 | mpdd 43 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β Ο β§ ((π₯ β π β§ π) β§ π)) β (π¦ β π₯ β ({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) β β
)) |
102 | 101 | necon2bd 2960 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β Ο β§ ((π₯ β π β§ π) β§ π)) β (({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) = β
β Β¬ π¦ β π₯)) |
103 | 102 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (π β Ο β (((π₯ β π β§ π) β§ π) β (({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) = β
β Β¬ π¦ β π₯))) |
104 | 103 | com23 86 |
. . . . . . . . . . . . . . . 16
β’ (π β Ο β (({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
β (((π₯ β π β§ π) β§ π) β Β¬ π¦ β π₯))) |
105 | 104 | imp31 419 |
. . . . . . . . . . . . . . 15
β’ (((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β§ ((π₯ β π β§ π) β§ π)) β Β¬ π¦ β π₯) |
106 | 105 | pm2.21d 121 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β§ ((π₯ β π β§ π) β§ π)) β (π¦ β π₯ β π₯ = π¦)) |
107 | | equcomi 2021 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π₯ β π₯ = π¦) |
108 | 107 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β§ ((π₯ β π β§ π) β§ π)) β (π¦ = π₯ β π₯ = π¦)) |
109 | 106, 108 | jaod 858 |
. . . . . . . . . . . . 13
β’ (((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β§ ((π₯ β π β§ π) β§ π)) β ((π¦ β π₯ β¨ π¦ = π₯) β π₯ = π¦)) |
110 | 32, 109 | biimtrid 241 |
. . . . . . . . . . . 12
β’ (((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β§ ((π₯ β π β§ π) β§ π)) β (π¦ β π₯ β π₯ = π¦)) |
111 | 110 | expr 458 |
. . . . . . . . . . 11
β’ (((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β§ (π₯ β π β§ π)) β (π β (π¦ β π₯ β π₯ = π¦))) |
112 | 111 | com23 86 |
. . . . . . . . . 10
β’ (((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β§ (π₯ β π β§ π)) β (π¦ β π₯ β (π β π₯ = π¦))) |
113 | 112 | impd 412 |
. . . . . . . . 9
β’ (((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β§ (π₯ β π β§ π)) β ((π¦ β π₯ β§ π) β π₯ = π¦)) |
114 | 113 | alrimiv 1931 |
. . . . . . . 8
β’ (((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β§ (π₯ β π β§ π)) β βπ¦((π¦ β π₯ β§ π) β π₯ = π¦)) |
115 | 31, 114 | jca 513 |
. . . . . . 7
β’ (((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β§ (π₯ β π β§ π)) β (π β§ βπ¦((π¦ β π₯ β§ π) β π₯ = π¦))) |
116 | 115 | ex 414 |
. . . . . 6
β’ ((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β ((π₯ β π β§ π) β (π β§ βπ¦((π¦ β π₯ β§ π) β π₯ = π¦)))) |
117 | 30, 116 | eximd 2210 |
. . . . 5
β’ ((π β Ο β§ ({π β Ο β£
βπ₯(π₯ β π β§ π)} β© π) = β
) β (βπ₯(π₯ β π β§ π) β βπ₯(π β§ βπ¦((π¦ β π₯ β§ π) β π₯ = π¦)))) |
118 | 117 | impancom 453 |
. . . 4
β’ ((π β Ο β§
βπ₯(π₯ β π β§ π)) β (({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) = β
β βπ₯(π β§ βπ¦((π¦ β π₯ β§ π) β π₯ = π¦)))) |
119 | 13, 118 | sylbi 216 |
. . 3
β’ (π β {π β Ο β£ βπ₯(π₯ β π β§ π)} β (({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) = β
β βπ₯(π β§ βπ¦((π¦ β π₯ β§ π) β π₯ = π¦)))) |
120 | 119 | rexlimiv 3146 |
. 2
β’
(βπ β
{π β Ο β£
βπ₯(π₯ β π β§ π)} ({π β Ο β£ βπ₯(π₯ β π β§ π)} β© π) = β
β βπ₯(π β§ βπ¦((π¦ β π₯ β§ π) β π₯ = π¦))) |
121 | 19, 25, 120 | 3syl 18 |
1
β’
(βπ₯ β Fin
π β βπ₯(π β§ βπ¦((π¦ β π₯ β§ π) β π₯ = π¦))) |