Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . 3
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β π΅ β
FinIII) |
2 | | simpll1 1213 |
. . . . . . 7
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β π΄ β π«
π΅) |
3 | 2 | adantr 482 |
. . . . . 6
β’
(((((π΄ β
π« π΅ β§
[β] Or π΄
β§ Β¬ βͺ π΄ β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII) β§ π β Ο) β π΄ β π« π΅) |
4 | | ssrab2 4042 |
. . . . . . . 8
β’ {π β π΄ β£ π βΌ π} β π΄ |
5 | 4 | unissi 4879 |
. . . . . . 7
β’ βͺ {π
β π΄ β£ π βΌ π} β βͺ π΄ |
6 | | sspwuni 5065 |
. . . . . . . 8
β’ (π΄ β π« π΅ β βͺ π΄
β π΅) |
7 | 6 | biimpi 215 |
. . . . . . 7
β’ (π΄ β π« π΅ β βͺ π΄
β π΅) |
8 | 5, 7 | sstrid 3960 |
. . . . . 6
β’ (π΄ β π« π΅ β βͺ {π
β π΄ β£ π βΌ π} β π΅) |
9 | 3, 8 | syl 17 |
. . . . 5
β’
(((((π΄ β
π« π΅ β§
[β] Or π΄
β§ Β¬ βͺ π΄ β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII) β§ π β Ο) β βͺ {π
β π΄ β£ π βΌ π} β π΅) |
10 | | elpw2g 5306 |
. . . . . 6
β’ (π΅ β FinIII β
(βͺ {π β π΄ β£ π βΌ π} β π« π΅ β βͺ {π β π΄ β£ π βΌ π} β π΅)) |
11 | 10 | ad2antlr 726 |
. . . . 5
β’
(((((π΄ β
π« π΅ β§
[β] Or π΄
β§ Β¬ βͺ π΄ β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII) β§ π β Ο) β (βͺ {π
β π΄ β£ π βΌ π} β π« π΅ β βͺ {π β π΄ β£ π βΌ π} β π΅)) |
12 | 9, 11 | mpbird 257 |
. . . 4
β’
(((((π΄ β
π« π΅ β§
[β] Or π΄
β§ Β¬ βͺ π΄ β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII) β§ π β Ο) β βͺ {π
β π΄ β£ π βΌ π} β π« π΅) |
13 | 12 | fmpttd 7068 |
. . 3
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β (π β Ο
β¦ βͺ {π β π΄ β£ π βΌ π}):ΟβΆπ« π΅) |
14 | | vex 3452 |
. . . . . . . . . . 11
β’ π β V |
15 | 14 | sucex 7746 |
. . . . . . . . . 10
β’ suc π β V |
16 | | sssucid 6402 |
. . . . . . . . . 10
β’ π β suc π |
17 | | ssdomg 8947 |
. . . . . . . . . 10
β’ (suc
π β V β (π β suc π β π βΌ suc π)) |
18 | 15, 16, 17 | mp2 9 |
. . . . . . . . 9
β’ π βΌ suc π |
19 | | domtr 8954 |
. . . . . . . . 9
β’ ((π βΌ π β§ π βΌ suc π) β π βΌ suc π) |
20 | 18, 19 | mpan2 690 |
. . . . . . . 8
β’ (π βΌ π β π βΌ suc π) |
21 | 20 | a1i 11 |
. . . . . . 7
β’ (π β π΄ β (π βΌ π β π βΌ suc π)) |
22 | 21 | ss2rabi 4039 |
. . . . . 6
β’ {π β π΄ β£ π βΌ π} β {π β π΄ β£ π βΌ suc π} |
23 | | uniss 4878 |
. . . . . 6
β’ ({π β π΄ β£ π βΌ π} β {π β π΄ β£ π βΌ suc π} β βͺ {π β π΄ β£ π βΌ π} β βͺ {π β π΄ β£ π βΌ suc π}) |
24 | 22, 23 | mp1i 13 |
. . . . 5
β’
(((((π΄ β
π« π΅ β§
[β] Or π΄
β§ Β¬ βͺ π΄ β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII) β§ π β Ο) β βͺ {π
β π΄ β£ π βΌ π} β βͺ {π β π΄ β£ π βΌ suc π}) |
25 | | id 22 |
. . . . . 6
β’ (π β Ο β π β
Ο) |
26 | | pwexg 5338 |
. . . . . . . . 9
β’ (π΅ β FinIII β
π« π΅ β
V) |
27 | 26 | adantl 483 |
. . . . . . . 8
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β π« π΅ β
V) |
28 | 27, 2 | ssexd 5286 |
. . . . . . 7
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β π΄ β
V) |
29 | | rabexg 5293 |
. . . . . . 7
β’ (π΄ β V β {π β π΄ β£ π βΌ π} β V) |
30 | | uniexg 7682 |
. . . . . . 7
β’ ({π β π΄ β£ π βΌ π} β V β βͺ {π
β π΄ β£ π βΌ π} β V) |
31 | 28, 29, 30 | 3syl 18 |
. . . . . 6
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β βͺ {π β π΄ β£ π βΌ π} β V) |
32 | | breq2 5114 |
. . . . . . . . 9
β’ (π = π β (π βΌ π β π βΌ π)) |
33 | 32 | rabbidv 3418 |
. . . . . . . 8
β’ (π = π β {π β π΄ β£ π βΌ π} = {π β π΄ β£ π βΌ π}) |
34 | 33 | unieqd 4884 |
. . . . . . 7
β’ (π = π β βͺ {π β π΄ β£ π βΌ π} = βͺ {π β π΄ β£ π βΌ π}) |
35 | | eqid 2737 |
. . . . . . 7
β’ (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) = (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) |
36 | 34, 35 | fvmptg 6951 |
. . . . . 6
β’ ((π β Ο β§ βͺ {π
β π΄ β£ π βΌ π} β V) β ((π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π})βπ) = βͺ {π β π΄ β£ π βΌ π}) |
37 | 25, 31, 36 | syl2anr 598 |
. . . . 5
β’
(((((π΄ β
π« π΅ β§
[β] Or π΄
β§ Β¬ βͺ π΄ β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII) β§ π β Ο) β ((π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π})βπ) = βͺ {π β π΄ β£ π βΌ π}) |
38 | | peano2 7832 |
. . . . . 6
β’ (π β Ο β suc π β
Ο) |
39 | | rabexg 5293 |
. . . . . . 7
β’ (π΄ β V β {π β π΄ β£ π βΌ suc π} β V) |
40 | | uniexg 7682 |
. . . . . . 7
β’ ({π β π΄ β£ π βΌ suc π} β V β βͺ {π
β π΄ β£ π βΌ suc π} β V) |
41 | 28, 39, 40 | 3syl 18 |
. . . . . 6
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β βͺ {π β π΄ β£ π βΌ suc π} β V) |
42 | | breq2 5114 |
. . . . . . . . 9
β’ (π = suc π β (π βΌ π β π βΌ suc π)) |
43 | 42 | rabbidv 3418 |
. . . . . . . 8
β’ (π = suc π β {π β π΄ β£ π βΌ π} = {π β π΄ β£ π βΌ suc π}) |
44 | 43 | unieqd 4884 |
. . . . . . 7
β’ (π = suc π β βͺ {π β π΄ β£ π βΌ π} = βͺ {π β π΄ β£ π βΌ suc π}) |
45 | 44, 35 | fvmptg 6951 |
. . . . . 6
β’ ((suc
π β Ο β§
βͺ {π β π΄ β£ π βΌ suc π} β V) β ((π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π})βsuc π) = βͺ {π β π΄ β£ π βΌ suc π}) |
46 | 38, 41, 45 | syl2anr 598 |
. . . . 5
β’
(((((π΄ β
π« π΅ β§
[β] Or π΄
β§ Β¬ βͺ π΄ β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII) β§ π β Ο) β ((π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π})βsuc π) = βͺ {π β π΄ β£ π βΌ suc π}) |
47 | 24, 37, 46 | 3sstr4d 3996 |
. . . 4
β’
(((((π΄ β
π« π΅ β§
[β] Or π΄
β§ Β¬ βͺ π΄ β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII) β§ π β Ο) β ((π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π})βπ) β ((π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π})βsuc π)) |
48 | 47 | ralrimiva 3144 |
. . 3
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β βπ β
Ο ((π β Ο
β¦ βͺ {π β π΄ β£ π βΌ π})βπ) β ((π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π})βsuc π)) |
49 | | fin34i 10324 |
. . 3
β’ ((π΅ β FinIII β§
(π β Ο β¦
βͺ {π β π΄ β£ π βΌ π}):ΟβΆπ« π΅ β§ βπ β Ο ((π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π})βπ) β ((π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π})βsuc π)) β βͺ ran
(π β Ο β¦
βͺ {π β π΄ β£ π βΌ π}) β ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π})) |
50 | 1, 13, 48, 49 | syl3anc 1372 |
. 2
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β βͺ ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) β ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π})) |
51 | | fin1a2lem11 10353 |
. . . . . 6
β’ ((
[β] Or π΄
β§ π΄ β Fin) β
ran (π β Ο
β¦ βͺ {π β π΄ β£ π βΌ π}) = (π΄ βͺ {β
})) |
52 | 51 | adantrr 716 |
. . . . 5
β’ ((
[β] Or π΄
β§ (π΄ β Fin β§
π΄ β β
)) β ran
(π β Ο β¦
βͺ {π β π΄ β£ π βΌ π}) = (π΄ βͺ {β
})) |
53 | 52 | 3ad2antl2 1187 |
. . . 4
β’ (((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β ran
(π β Ο β¦
βͺ {π β π΄ β£ π βΌ π}) = (π΄ βͺ {β
})) |
54 | 53 | adantr 482 |
. . 3
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β ran (π β
Ο β¦ βͺ {π β π΄ β£ π βΌ π}) = (π΄ βͺ {β
})) |
55 | | simpll3 1215 |
. . . . . 6
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β Β¬ βͺ π΄ β π΄) |
56 | | simplrr 777 |
. . . . . . 7
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β π΄ β
β
) |
57 | | sspwuni 5065 |
. . . . . . . . . . 11
β’ (π΄ β π« β
β βͺ π΄ β β
) |
58 | | ss0b 4362 |
. . . . . . . . . . 11
β’ (βͺ π΄
β β
β βͺ π΄ = β
) |
59 | 57, 58 | bitri 275 |
. . . . . . . . . 10
β’ (π΄ β π« β
β βͺ π΄ = β
) |
60 | | pw0 4777 |
. . . . . . . . . . . . 13
β’ π«
β
= {β
} |
61 | 60 | sseq2i 3978 |
. . . . . . . . . . . 12
β’ (π΄ β π« β
β π΄ β
{β
}) |
62 | | sssn 4791 |
. . . . . . . . . . . 12
β’ (π΄ β {β
} β (π΄ = β
β¨ π΄ = {β
})) |
63 | 61, 62 | bitri 275 |
. . . . . . . . . . 11
β’ (π΄ β π« β
β (π΄ = β
β¨
π΄ =
{β
})) |
64 | | df-ne 2945 |
. . . . . . . . . . . 12
β’ (π΄ β β
β Β¬ π΄ = β
) |
65 | | 0ex 5269 |
. . . . . . . . . . . . . . . . 17
β’ β
β V |
66 | 65 | unisn 4892 |
. . . . . . . . . . . . . . . 16
β’ βͺ {β
} = β
|
67 | 65 | snid 4627 |
. . . . . . . . . . . . . . . 16
β’ β
β {β
} |
68 | 66, 67 | eqeltri 2834 |
. . . . . . . . . . . . . . 15
β’ βͺ {β
} β {β
} |
69 | | unieq 4881 |
. . . . . . . . . . . . . . . 16
β’ (π΄ = {β
} β βͺ π΄ =
βͺ {β
}) |
70 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π΄ = {β
} β π΄ = {β
}) |
71 | 69, 70 | eleq12d 2832 |
. . . . . . . . . . . . . . 15
β’ (π΄ = {β
} β (βͺ π΄
β π΄ β βͺ {β
} β {β
})) |
72 | 68, 71 | mpbiri 258 |
. . . . . . . . . . . . . 14
β’ (π΄ = {β
} β βͺ π΄
β π΄) |
73 | 72 | orim2i 910 |
. . . . . . . . . . . . 13
β’ ((π΄ = β
β¨ π΄ = {β
}) β (π΄ = β
β¨ βͺ π΄
β π΄)) |
74 | 73 | ord 863 |
. . . . . . . . . . . 12
β’ ((π΄ = β
β¨ π΄ = {β
}) β (Β¬
π΄ = β
β βͺ π΄
β π΄)) |
75 | 64, 74 | biimtrid 241 |
. . . . . . . . . . 11
β’ ((π΄ = β
β¨ π΄ = {β
}) β (π΄ β β
β βͺ π΄
β π΄)) |
76 | 63, 75 | sylbi 216 |
. . . . . . . . . 10
β’ (π΄ β π« β
β (π΄ β β
β βͺ π΄ β π΄)) |
77 | 59, 76 | sylbir 234 |
. . . . . . . . 9
β’ (βͺ π΄ =
β
β (π΄ β
β
β βͺ π΄ β π΄)) |
78 | 77 | com12 32 |
. . . . . . . 8
β’ (π΄ β β
β (βͺ π΄ =
β
β βͺ π΄ β π΄)) |
79 | 78 | con3d 152 |
. . . . . . 7
β’ (π΄ β β
β (Β¬
βͺ π΄ β π΄ β Β¬ βͺ
π΄ =
β
)) |
80 | 56, 55, 79 | sylc 65 |
. . . . . 6
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β Β¬ βͺ π΄ = β
) |
81 | | ioran 983 |
. . . . . 6
β’ (Β¬
(βͺ π΄ β π΄ β¨ βͺ π΄ = β
) β (Β¬ βͺ π΄
β π΄ β§ Β¬ βͺ π΄ =
β
)) |
82 | 55, 80, 81 | sylanbrc 584 |
. . . . 5
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β Β¬ (βͺ π΄ β π΄ β¨ βͺ π΄ = β
)) |
83 | | uniun 4896 |
. . . . . . . 8
β’ βͺ (π΄
βͺ {β
}) = (βͺ π΄ βͺ βͺ
{β
}) |
84 | 66 | uneq2i 4125 |
. . . . . . . 8
β’ (βͺ π΄
βͺ βͺ {β
}) = (βͺ
π΄ βͺ
β
) |
85 | | un0 4355 |
. . . . . . . 8
β’ (βͺ π΄
βͺ β
) = βͺ π΄ |
86 | 83, 84, 85 | 3eqtri 2769 |
. . . . . . 7
β’ βͺ (π΄
βͺ {β
}) = βͺ π΄ |
87 | 86 | eleq1i 2829 |
. . . . . 6
β’ (βͺ (π΄
βͺ {β
}) β (π΄
βͺ {β
}) β βͺ π΄ β (π΄ βͺ {β
})) |
88 | | elun 4113 |
. . . . . 6
β’ (βͺ π΄
β (π΄ βͺ {β
})
β (βͺ π΄ β π΄ β¨ βͺ π΄ β
{β
})) |
89 | 65 | elsn2 4630 |
. . . . . . 7
β’ (βͺ π΄
β {β
} β βͺ π΄ = β
) |
90 | 89 | orbi2i 912 |
. . . . . 6
β’ ((βͺ π΄
β π΄ β¨ βͺ π΄
β {β
}) β (βͺ π΄ β π΄ β¨ βͺ π΄ = β
)) |
91 | 87, 88, 90 | 3bitri 297 |
. . . . 5
β’ (βͺ (π΄
βͺ {β
}) β (π΄
βͺ {β
}) β (βͺ π΄ β π΄ β¨ βͺ π΄ = β
)) |
92 | 82, 91 | sylnibr 329 |
. . . 4
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β Β¬ βͺ (π΄ βͺ {β
}) β (π΄ βͺ {β
})) |
93 | | unieq 4881 |
. . . . . 6
β’ (ran
(π β Ο β¦
βͺ {π β π΄ β£ π βΌ π}) = (π΄ βͺ {β
}) β βͺ ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) = βͺ (π΄ βͺ
{β
})) |
94 | | id 22 |
. . . . . 6
β’ (ran
(π β Ο β¦
βͺ {π β π΄ β£ π βΌ π}) = (π΄ βͺ {β
}) β ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) = (π΄ βͺ {β
})) |
95 | 93, 94 | eleq12d 2832 |
. . . . 5
β’ (ran
(π β Ο β¦
βͺ {π β π΄ β£ π βΌ π}) = (π΄ βͺ {β
}) β (βͺ ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) β ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) β βͺ (π΄ βͺ {β
}) β (π΄ βͺ
{β
}))) |
96 | 95 | notbid 318 |
. . . 4
β’ (ran
(π β Ο β¦
βͺ {π β π΄ β£ π βΌ π}) = (π΄ βͺ {β
}) β (Β¬ βͺ ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) β ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) β Β¬ βͺ
(π΄ βͺ {β
}) β
(π΄ βͺ
{β
}))) |
97 | 92, 96 | syl5ibrcom 247 |
. . 3
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β (ran (π β
Ο β¦ βͺ {π β π΄ β£ π βΌ π}) = (π΄ βͺ {β
}) β Β¬ βͺ ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) β ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}))) |
98 | 54, 97 | mpd 15 |
. 2
β’ ((((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β§ π΅ β FinIII)
β Β¬ βͺ ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π}) β ran (π β Ο β¦ βͺ {π
β π΄ β£ π βΌ π})) |
99 | 50, 98 | pm2.65da 816 |
1
β’ (((π΄ β π« π΅ β§ [β] Or
π΄ β§ Β¬ βͺ π΄
β π΄) β§ (π΄ β Fin β§ π΄ β β
)) β Β¬
π΅ β
FinIII) |