Step | Hyp | Ref
| Expression |
1 | | fvex 6905 |
. . 3
β’
(cardβπ΅)
β V |
2 | | ssid 4005 |
. . . . . . 7
β’
(cardβπ΅)
β (cardβπ΅) |
3 | | cfslb.1 |
. . . . . . . . . . 11
β’ π΄ β V |
4 | 3 | ssex 5322 |
. . . . . . . . . 10
β’ (π΅ β π΄ β π΅ β V) |
5 | 4 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π΅ β π΄ β§ βͺ π΅ = π΄) β§ (cardβπ΅) β (cardβπ΅)) β π΅ β V) |
6 | | velpw 4608 |
. . . . . . . . . . . . 13
β’ (π₯ β π« π΄ β π₯ β π΄) |
7 | | sseq1 4008 |
. . . . . . . . . . . . 13
β’ (π₯ = π΅ β (π₯ β π΄ β π΅ β π΄)) |
8 | 6, 7 | bitrid 283 |
. . . . . . . . . . . 12
β’ (π₯ = π΅ β (π₯ β π« π΄ β π΅ β π΄)) |
9 | | unieq 4920 |
. . . . . . . . . . . . 13
β’ (π₯ = π΅ β βͺ π₯ = βͺ
π΅) |
10 | 9 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ (π₯ = π΅ β (βͺ π₯ = π΄ β βͺ π΅ = π΄)) |
11 | 8, 10 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π₯ = π΅ β ((π₯ β π« π΄ β§ βͺ π₯ = π΄) β (π΅ β π΄ β§ βͺ π΅ = π΄))) |
12 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π₯ = π΅ β (cardβπ₯) = (cardβπ΅)) |
13 | 12 | sseq1d 4014 |
. . . . . . . . . . 11
β’ (π₯ = π΅ β ((cardβπ₯) β (cardβπ΅) β (cardβπ΅) β (cardβπ΅))) |
14 | 11, 13 | anbi12d 632 |
. . . . . . . . . 10
β’ (π₯ = π΅ β (((π₯ β π« π΄ β§ βͺ π₯ = π΄) β§ (cardβπ₯) β (cardβπ΅)) β ((π΅ β π΄ β§ βͺ π΅ = π΄) β§ (cardβπ΅) β (cardβπ΅)))) |
15 | 14 | spcegv 3588 |
. . . . . . . . 9
β’ (π΅ β V β (((π΅ β π΄ β§ βͺ π΅ = π΄) β§ (cardβπ΅) β (cardβπ΅)) β βπ₯((π₯ β π« π΄ β§ βͺ π₯ = π΄) β§ (cardβπ₯) β (cardβπ΅)))) |
16 | 5, 15 | mpcom 38 |
. . . . . . . 8
β’ (((π΅ β π΄ β§ βͺ π΅ = π΄) β§ (cardβπ΅) β (cardβπ΅)) β βπ₯((π₯ β π« π΄ β§ βͺ π₯ = π΄) β§ (cardβπ₯) β (cardβπ΅))) |
17 | | df-rex 3072 |
. . . . . . . . 9
β’
(βπ₯ β
{π₯ β π« π΄ β£ βͺ π₯ =
π΄} (cardβπ₯) β (cardβπ΅) β βπ₯(π₯ β {π₯ β π« π΄ β£ βͺ π₯ = π΄} β§ (cardβπ₯) β (cardβπ΅))) |
18 | | rabid 3453 |
. . . . . . . . . . 11
β’ (π₯ β {π₯ β π« π΄ β£ βͺ π₯ = π΄} β (π₯ β π« π΄ β§ βͺ π₯ = π΄)) |
19 | 18 | anbi1i 625 |
. . . . . . . . . 10
β’ ((π₯ β {π₯ β π« π΄ β£ βͺ π₯ = π΄} β§ (cardβπ₯) β (cardβπ΅)) β ((π₯ β π« π΄ β§ βͺ π₯ = π΄) β§ (cardβπ₯) β (cardβπ΅))) |
20 | 19 | exbii 1851 |
. . . . . . . . 9
β’
(βπ₯(π₯ β {π₯ β π« π΄ β£ βͺ π₯ = π΄} β§ (cardβπ₯) β (cardβπ΅)) β βπ₯((π₯ β π« π΄ β§ βͺ π₯ = π΄) β§ (cardβπ₯) β (cardβπ΅))) |
21 | 17, 20 | bitri 275 |
. . . . . . . 8
β’
(βπ₯ β
{π₯ β π« π΄ β£ βͺ π₯ =
π΄} (cardβπ₯) β (cardβπ΅) β βπ₯((π₯ β π« π΄ β§ βͺ π₯ = π΄) β§ (cardβπ₯) β (cardβπ΅))) |
22 | 16, 21 | sylibr 233 |
. . . . . . 7
β’ (((π΅ β π΄ β§ βͺ π΅ = π΄) β§ (cardβπ΅) β (cardβπ΅)) β βπ₯ β {π₯ β π« π΄ β£ βͺ π₯ = π΄} (cardβπ₯) β (cardβπ΅)) |
23 | 2, 22 | mpan2 690 |
. . . . . 6
β’ ((π΅ β π΄ β§ βͺ π΅ = π΄) β βπ₯ β {π₯ β π« π΄ β£ βͺ π₯ = π΄} (cardβπ₯) β (cardβπ΅)) |
24 | | iinss 5060 |
. . . . . 6
β’
(βπ₯ β
{π₯ β π« π΄ β£ βͺ π₯ =
π΄} (cardβπ₯) β (cardβπ΅) β β© π₯ β {π₯ β π« π΄ β£ βͺ π₯ = π΄} (cardβπ₯) β (cardβπ΅)) |
25 | 23, 24 | syl 17 |
. . . . 5
β’ ((π΅ β π΄ β§ βͺ π΅ = π΄) β β©
π₯ β {π₯ β π« π΄ β£ βͺ π₯ =
π΄} (cardβπ₯) β (cardβπ΅)) |
26 | 3 | cflim3 10257 |
. . . . . 6
β’ (Lim
π΄ β (cfβπ΄) = β© π₯ β {π₯ β π« π΄ β£ βͺ π₯ = π΄} (cardβπ₯)) |
27 | 26 | sseq1d 4014 |
. . . . 5
β’ (Lim
π΄ β ((cfβπ΄) β (cardβπ΅) β β© π₯ β {π₯ β π« π΄ β£ βͺ π₯ = π΄} (cardβπ₯) β (cardβπ΅))) |
28 | 25, 27 | imbitrrid 245 |
. . . 4
β’ (Lim
π΄ β ((π΅ β π΄ β§ βͺ π΅ = π΄) β (cfβπ΄) β (cardβπ΅))) |
29 | 28 | 3impib 1117 |
. . 3
β’ ((Lim
π΄ β§ π΅ β π΄ β§ βͺ π΅ = π΄) β (cfβπ΄) β (cardβπ΅)) |
30 | | ssdomg 8996 |
. . 3
β’
((cardβπ΅)
β V β ((cfβπ΄) β (cardβπ΅) β (cfβπ΄) βΌ (cardβπ΅))) |
31 | 1, 29, 30 | mpsyl 68 |
. 2
β’ ((Lim
π΄ β§ π΅ β π΄ β§ βͺ π΅ = π΄) β (cfβπ΄) βΌ (cardβπ΅)) |
32 | | limord 6425 |
. . . . . . 7
β’ (Lim
π΄ β Ord π΄) |
33 | | ordsson 7770 |
. . . . . . 7
β’ (Ord
π΄ β π΄ β On) |
34 | 32, 33 | syl 17 |
. . . . . 6
β’ (Lim
π΄ β π΄ β On) |
35 | | sstr2 3990 |
. . . . . 6
β’ (π΅ β π΄ β (π΄ β On β π΅ β On)) |
36 | 34, 35 | mpan9 508 |
. . . . 5
β’ ((Lim
π΄ β§ π΅ β π΄) β π΅ β On) |
37 | | onssnum 10035 |
. . . . 5
β’ ((π΅ β V β§ π΅ β On) β π΅ β dom
card) |
38 | 4, 36, 37 | syl2an2 685 |
. . . 4
β’ ((Lim
π΄ β§ π΅ β π΄) β π΅ β dom card) |
39 | | cardid2 9948 |
. . . 4
β’ (π΅ β dom card β
(cardβπ΅) β
π΅) |
40 | 38, 39 | syl 17 |
. . 3
β’ ((Lim
π΄ β§ π΅ β π΄) β (cardβπ΅) β π΅) |
41 | 40 | 3adant3 1133 |
. 2
β’ ((Lim
π΄ β§ π΅ β π΄ β§ βͺ π΅ = π΄) β (cardβπ΅) β π΅) |
42 | | domentr 9009 |
. 2
β’
(((cfβπ΄)
βΌ (cardβπ΅)
β§ (cardβπ΅)
β π΅) β
(cfβπ΄) βΌ π΅) |
43 | 31, 41, 42 | syl2anc 585 |
1
β’ ((Lim
π΄ β§ π΅ β π΄ β§ βͺ π΅ = π΄) β (cfβπ΄) βΌ π΅) |