Step | Hyp | Ref
| Expression |
1 | | ssid 4005 |
. . 3
β’ π΄ β π΄ |
2 | | ssid 4005 |
. . . . 5
β’ π§ β π§ |
3 | | sseq2 4009 |
. . . . . 6
β’ (π€ = π§ β (π§ β π€ β π§ β π§)) |
4 | 3 | rspcev 3613 |
. . . . 5
β’ ((π§ β π΄ β§ π§ β π§) β βπ€ β π΄ π§ β π€) |
5 | 2, 4 | mpan2 690 |
. . . 4
β’ (π§ β π΄ β βπ€ β π΄ π§ β π€) |
6 | 5 | rgen 3064 |
. . 3
β’
βπ§ β
π΄ βπ€ β π΄ π§ β π€ |
7 | | sseq1 4008 |
. . . . 5
β’ (π¦ = π΄ β (π¦ β π΄ β π΄ β π΄)) |
8 | | rexeq 3322 |
. . . . . 6
β’ (π¦ = π΄ β (βπ€ β π¦ π§ β π€ β βπ€ β π΄ π§ β π€)) |
9 | 8 | ralbidv 3178 |
. . . . 5
β’ (π¦ = π΄ β (βπ§ β π΄ βπ€ β π¦ π§ β π€ β βπ§ β π΄ βπ€ β π΄ π§ β π€)) |
10 | 7, 9 | anbi12d 632 |
. . . 4
β’ (π¦ = π΄ β ((π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€) β (π΄ β π΄ β§ βπ§ β π΄ βπ€ β π΄ π§ β π€))) |
11 | 10 | spcegv 3588 |
. . 3
β’ (π΄ β π β ((π΄ β π΄ β§ βπ§ β π΄ βπ€ β π΄ π§ β π€) β βπ¦(π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))) |
12 | 1, 6, 11 | mp2ani 697 |
. 2
β’ (π΄ β π β βπ¦(π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) |
13 | | fvex 6905 |
. . . . . 6
β’
(cardβπ¦)
β V |
14 | 13 | isseti 3490 |
. . . . 5
β’
βπ₯ π₯ = (cardβπ¦) |
15 | | 19.41v 1954 |
. . . . 5
β’
(βπ₯(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (βπ₯ π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))) |
16 | 14, 15 | mpbiran 708 |
. . . 4
β’
(βπ₯(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) |
17 | 16 | exbii 1851 |
. . 3
β’
(βπ¦βπ₯(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β βπ¦(π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) |
18 | | excom 2163 |
. . 3
β’
(βπ¦βπ₯(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€)) β βπ₯βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))) |
19 | 17, 18 | bitr3i 277 |
. 2
β’
(βπ¦(π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€) β βπ₯βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))) |
20 | 12, 19 | sylib 217 |
1
β’ (π΄ β π β βπ₯βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ€ β π¦ π§ β π€))) |