Step | Hyp | Ref
| Expression |
1 | | elex 3493 |
. 2
β’ (π΄ β π΅ β π΄ β V) |
2 | | isinfcard 10087 |
. . . . . . . . . . . . 13
β’ ((Ο
β (πΉβπ₯) β§ (cardβ(πΉβπ₯)) = (πΉβπ₯)) β (πΉβπ₯) β ran β΅) |
3 | 2 | bicomi 223 |
. . . . . . . . . . . 12
β’ ((πΉβπ₯) β ran β΅ β (Ο β
(πΉβπ₯) β§ (cardβ(πΉβπ₯)) = (πΉβπ₯))) |
4 | 3 | simplbi 499 |
. . . . . . . . . . 11
β’ ((πΉβπ₯) β ran β΅ β Ο β
(πΉβπ₯)) |
5 | | ffn 6718 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆ(Ο βͺ ran β΅) β
πΉ Fn π΄) |
6 | | fnfvelrn 7083 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ Fn π΄ β§ π₯ β π΄) β (πΉβπ₯) β ran πΉ) |
7 | 6 | ex 414 |
. . . . . . . . . . . . . . 15
β’ (πΉ Fn π΄ β (π₯ β π΄ β (πΉβπ₯) β ran πΉ)) |
8 | | fnima 6681 |
. . . . . . . . . . . . . . . 16
β’ (πΉ Fn π΄ β (πΉ β π΄) = ran πΉ) |
9 | 8 | eleq2d 2820 |
. . . . . . . . . . . . . . 15
β’ (πΉ Fn π΄ β ((πΉβπ₯) β (πΉ β π΄) β (πΉβπ₯) β ran πΉ)) |
10 | 7, 9 | sylibrd 259 |
. . . . . . . . . . . . . 14
β’ (πΉ Fn π΄ β (π₯ β π΄ β (πΉβπ₯) β (πΉ β π΄))) |
11 | | elssuni 4942 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ₯) β (πΉ β π΄) β (πΉβπ₯) β βͺ (πΉ β π΄)) |
12 | 10, 11 | syl6 35 |
. . . . . . . . . . . . 13
β’ (πΉ Fn π΄ β (π₯ β π΄ β (πΉβπ₯) β βͺ (πΉ β π΄))) |
13 | 12 | imp 408 |
. . . . . . . . . . . 12
β’ ((πΉ Fn π΄ β§ π₯ β π΄) β (πΉβπ₯) β βͺ (πΉ β π΄)) |
14 | 5, 13 | sylan 581 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
π₯ β π΄) β (πΉβπ₯) β βͺ (πΉ β π΄)) |
15 | 4, 14 | sylan9ssr 3997 |
. . . . . . . . . 10
β’ (((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
π₯ β π΄) β§ (πΉβπ₯) β ran β΅) β Ο β
βͺ (πΉ β π΄)) |
16 | 15 | anasss 468 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
(π₯ β π΄ β§ (πΉβπ₯) β ran β΅)) β Ο β
βͺ (πΉ β π΄)) |
17 | 16 | a1i 11 |
. . . . . . . 8
β’ (π΄ β V β ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
(π₯ β π΄ β§ (πΉβπ₯) β ran β΅)) β Ο β
βͺ (πΉ β π΄))) |
18 | | carduniima 10091 |
. . . . . . . . . 10
β’ (π΄ β V β (πΉ:π΄βΆ(Ο βͺ ran β΅) β
βͺ (πΉ β π΄) β (Ο βͺ ran
β΅))) |
19 | | iscard3 10088 |
. . . . . . . . . 10
β’
((cardββͺ (πΉ β π΄)) = βͺ (πΉ β π΄) β βͺ (πΉ β π΄) β (Ο βͺ ran
β΅)) |
20 | 18, 19 | imbitrrdi 251 |
. . . . . . . . 9
β’ (π΄ β V β (πΉ:π΄βΆ(Ο βͺ ran β΅) β
(cardββͺ (πΉ β π΄)) = βͺ (πΉ β π΄))) |
21 | 20 | adantrd 493 |
. . . . . . . 8
β’ (π΄ β V β ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
(π₯ β π΄ β§ (πΉβπ₯) β ran β΅)) β
(cardββͺ (πΉ β π΄)) = βͺ (πΉ β π΄))) |
22 | 17, 21 | jcad 514 |
. . . . . . 7
β’ (π΄ β V β ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
(π₯ β π΄ β§ (πΉβπ₯) β ran β΅)) β (Ο
β βͺ (πΉ β π΄) β§ (cardββͺ (πΉ
β π΄)) = βͺ (πΉ
β π΄)))) |
23 | | isinfcard 10087 |
. . . . . . 7
β’ ((Ο
β βͺ (πΉ β π΄) β§ (cardββͺ (πΉ
β π΄)) = βͺ (πΉ
β π΄)) β βͺ (πΉ
β π΄) β ran
β΅) |
24 | 22, 23 | imbitrdi 250 |
. . . . . 6
β’ (π΄ β V β ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
(π₯ β π΄ β§ (πΉβπ₯) β ran β΅)) β βͺ (πΉ
β π΄) β ran
β΅)) |
25 | 24 | exp4d 435 |
. . . . 5
β’ (π΄ β V β (πΉ:π΄βΆ(Ο βͺ ran β΅) β
(π₯ β π΄ β ((πΉβπ₯) β ran β΅ β βͺ (πΉ
β π΄) β ran
β΅)))) |
26 | 25 | imp 408 |
. . . 4
β’ ((π΄ β V β§ πΉ:π΄βΆ(Ο βͺ ran β΅)) β
(π₯ β π΄ β ((πΉβπ₯) β ran β΅ β βͺ (πΉ
β π΄) β ran
β΅))) |
27 | 26 | rexlimdv 3154 |
. . 3
β’ ((π΄ β V β§ πΉ:π΄βΆ(Ο βͺ ran β΅)) β
(βπ₯ β π΄ (πΉβπ₯) β ran β΅ β βͺ (πΉ
β π΄) β ran
β΅)) |
28 | 27 | expimpd 455 |
. 2
β’ (π΄ β V β ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
βπ₯ β π΄ (πΉβπ₯) β ran β΅) β βͺ (πΉ
β π΄) β ran
β΅)) |
29 | 1, 28 | syl 17 |
1
β’ (π΄ β π΅ β ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
βπ₯ β π΄ (πΉβπ₯) β ran β΅) β βͺ (πΉ
β π΄) β ran
β΅)) |