Step | Hyp | Ref
| Expression |
1 | | elex 3491 |
. 2
β’ (π΄ β π΅ β π΄ β V) |
2 | | isinfcard 10089 |
. . . . . . . . . . . . 13
β’ ((Ο
β (πΉβπ₯) β§ (cardβ(πΉβπ₯)) = (πΉβπ₯)) β (πΉβπ₯) β ran β΅) |
3 | 2 | bicomi 223 |
. . . . . . . . . . . 12
β’ ((πΉβπ₯) β ran β΅ β (Ο β
(πΉβπ₯) β§ (cardβ(πΉβπ₯)) = (πΉβπ₯))) |
4 | 3 | simplbi 496 |
. . . . . . . . . . 11
β’ ((πΉβπ₯) β ran β΅ β Ο β
(πΉβπ₯)) |
5 | | ffn 6716 |
. . . . . . . . . . . 12
β’ (πΉ:π΄βΆ(Ο βͺ ran β΅) β
πΉ Fn π΄) |
6 | | fnfvelrn 7081 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ Fn π΄ β§ π₯ β π΄) β (πΉβπ₯) β ran πΉ) |
7 | 6 | ex 411 |
. . . . . . . . . . . . . . 15
β’ (πΉ Fn π΄ β (π₯ β π΄ β (πΉβπ₯) β ran πΉ)) |
8 | | fnima 6679 |
. . . . . . . . . . . . . . . 16
β’ (πΉ Fn π΄ β (πΉ β π΄) = ran πΉ) |
9 | 8 | eleq2d 2817 |
. . . . . . . . . . . . . . 15
β’ (πΉ Fn π΄ β ((πΉβπ₯) β (πΉ β π΄) β (πΉβπ₯) β ran πΉ)) |
10 | 7, 9 | sylibrd 258 |
. . . . . . . . . . . . . 14
β’ (πΉ Fn π΄ β (π₯ β π΄ β (πΉβπ₯) β (πΉ β π΄))) |
11 | | elssuni 4940 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ₯) β (πΉ β π΄) β (πΉβπ₯) β βͺ (πΉ β π΄)) |
12 | 10, 11 | syl6 35 |
. . . . . . . . . . . . 13
β’ (πΉ Fn π΄ β (π₯ β π΄ β (πΉβπ₯) β βͺ (πΉ β π΄))) |
13 | 12 | imp 405 |
. . . . . . . . . . . 12
β’ ((πΉ Fn π΄ β§ π₯ β π΄) β (πΉβπ₯) β βͺ (πΉ β π΄)) |
14 | 5, 13 | sylan 578 |
. . . . . . . . . . 11
β’ ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
π₯ β π΄) β (πΉβπ₯) β βͺ (πΉ β π΄)) |
15 | 4, 14 | sylan9ssr 3995 |
. . . . . . . . . 10
β’ (((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
π₯ β π΄) β§ (πΉβπ₯) β ran β΅) β Ο β
βͺ (πΉ β π΄)) |
16 | 15 | anasss 465 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
(π₯ β π΄ β§ (πΉβπ₯) β ran β΅)) β Ο β
βͺ (πΉ β π΄)) |
17 | 16 | a1i 11 |
. . . . . . . 8
β’ (π΄ β V β ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
(π₯ β π΄ β§ (πΉβπ₯) β ran β΅)) β Ο β
βͺ (πΉ β π΄))) |
18 | | carduniima 10093 |
. . . . . . . . . 10
β’ (π΄ β V β (πΉ:π΄βΆ(Ο βͺ ran β΅) β
βͺ (πΉ β π΄) β (Ο βͺ ran
β΅))) |
19 | | iscard3 10090 |
. . . . . . . . . 10
β’
((cardββͺ (πΉ β π΄)) = βͺ (πΉ β π΄) β βͺ (πΉ β π΄) β (Ο βͺ ran
β΅)) |
20 | 18, 19 | imbitrrdi 251 |
. . . . . . . . 9
β’ (π΄ β V β (πΉ:π΄βΆ(Ο βͺ ran β΅) β
(cardββͺ (πΉ β π΄)) = βͺ (πΉ β π΄))) |
21 | 20 | adantrd 490 |
. . . . . . . 8
β’ (π΄ β V β ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
(π₯ β π΄ β§ (πΉβπ₯) β ran β΅)) β
(cardββͺ (πΉ β π΄)) = βͺ (πΉ β π΄))) |
22 | 17, 21 | jcad 511 |
. . . . . . 7
β’ (π΄ β V β ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
(π₯ β π΄ β§ (πΉβπ₯) β ran β΅)) β (Ο
β βͺ (πΉ β π΄) β§ (cardββͺ (πΉ
β π΄)) = βͺ (πΉ
β π΄)))) |
23 | | isinfcard 10089 |
. . . . . . 7
β’ ((Ο
β βͺ (πΉ β π΄) β§ (cardββͺ (πΉ
β π΄)) = βͺ (πΉ
β π΄)) β βͺ (πΉ
β π΄) β ran
β΅) |
24 | 22, 23 | imbitrdi 250 |
. . . . . 6
β’ (π΄ β V β ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
(π₯ β π΄ β§ (πΉβπ₯) β ran β΅)) β βͺ (πΉ
β π΄) β ran
β΅)) |
25 | 24 | exp4d 432 |
. . . . 5
β’ (π΄ β V β (πΉ:π΄βΆ(Ο βͺ ran β΅) β
(π₯ β π΄ β ((πΉβπ₯) β ran β΅ β βͺ (πΉ
β π΄) β ran
β΅)))) |
26 | 25 | imp 405 |
. . . 4
β’ ((π΄ β V β§ πΉ:π΄βΆ(Ο βͺ ran β΅)) β
(π₯ β π΄ β ((πΉβπ₯) β ran β΅ β βͺ (πΉ
β π΄) β ran
β΅))) |
27 | 26 | rexlimdv 3151 |
. . 3
β’ ((π΄ β V β§ πΉ:π΄βΆ(Ο βͺ ran β΅)) β
(βπ₯ β π΄ (πΉβπ₯) β ran β΅ β βͺ (πΉ
β π΄) β ran
β΅)) |
28 | 27 | expimpd 452 |
. 2
β’ (π΄ β V β ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
βπ₯ β π΄ (πΉβπ₯) β ran β΅) β βͺ (πΉ
β π΄) β ran
β΅)) |
29 | 1, 28 | syl 17 |
1
β’ (π΄ β π΅ β ((πΉ:π΄βΆ(Ο βͺ ran β΅) β§
βπ₯ β π΄ (πΉβπ₯) β ran β΅) β βͺ (πΉ
β π΄) β ran
β΅)) |