Step | Hyp | Ref
| Expression |
1 | | vex 3479 |
. . . . . 6
β’ π¦ β V |
2 | 1 | brdom 8956 |
. . . . 5
β’ (π΄ βΌ π¦ β βπ π:π΄β1-1βπ¦) |
3 | | f1f 6788 |
. . . . . . . . . . . 12
β’ (π:π΄β1-1βπ¦ β π:π΄βΆπ¦) |
4 | 3 | frnd 6726 |
. . . . . . . . . . 11
β’ (π:π΄β1-1βπ¦ β ran π β π¦) |
5 | | onss 7772 |
. . . . . . . . . . 11
β’ (π¦ β On β π¦ β On) |
6 | | sstr2 3990 |
. . . . . . . . . . 11
β’ (ran
π β π¦ β (π¦ β On β ran π β On)) |
7 | 4, 5, 6 | syl2im 40 |
. . . . . . . . . 10
β’ (π:π΄β1-1βπ¦ β (π¦ β On β ran π β On)) |
8 | | epweon 7762 |
. . . . . . . . . 10
β’ E We
On |
9 | | wess 5664 |
. . . . . . . . . 10
β’ (ran
π β On β ( E We
On β E We ran π)) |
10 | 7, 8, 9 | syl6mpi 67 |
. . . . . . . . 9
β’ (π:π΄β1-1βπ¦ β (π¦ β On β E We ran π)) |
11 | 10 | adantl 483 |
. . . . . . . 8
β’ ((π΄ βΌ π¦ β§ π:π΄β1-1βπ¦) β (π¦ β On β E We ran π)) |
12 | | f1f1orn 6845 |
. . . . . . . . . 10
β’ (π:π΄β1-1βπ¦ β π:π΄β1-1-ontoβran
π) |
13 | | eqid 2733 |
. . . . . . . . . . 11
β’
{β¨π€, π§β© β£ (πβπ€) E (πβπ§)} = {β¨π€, π§β© β£ (πβπ€) E (πβπ§)} |
14 | 13 | f1owe 7350 |
. . . . . . . . . 10
β’ (π:π΄β1-1-ontoβran
π β ( E We ran π β {β¨π€, π§β© β£ (πβπ€) E (πβπ§)} We π΄)) |
15 | 12, 14 | syl 17 |
. . . . . . . . 9
β’ (π:π΄β1-1βπ¦ β ( E We ran π β {β¨π€, π§β© β£ (πβπ€) E (πβπ§)} We π΄)) |
16 | | weinxp 5761 |
. . . . . . . . . 10
β’
({β¨π€, π§β© β£ (πβπ€) E (πβπ§)} We π΄ β ({β¨π€, π§β© β£ (πβπ€) E (πβπ§)} β© (π΄ Γ π΄)) We π΄) |
17 | | reldom 8945 |
. . . . . . . . . . . 12
β’ Rel
βΌ |
18 | 17 | brrelex1i 5733 |
. . . . . . . . . . 11
β’ (π΄ βΌ π¦ β π΄ β V) |
19 | | sqxpexg 7742 |
. . . . . . . . . . 11
β’ (π΄ β V β (π΄ Γ π΄) β V) |
20 | | incom 4202 |
. . . . . . . . . . . 12
β’ ((π΄ Γ π΄) β© {β¨π€, π§β© β£ (πβπ€) E (πβπ§)}) = ({β¨π€, π§β© β£ (πβπ€) E (πβπ§)} β© (π΄ Γ π΄)) |
21 | | inex1g 5320 |
. . . . . . . . . . . 12
β’ ((π΄ Γ π΄) β V β ((π΄ Γ π΄) β© {β¨π€, π§β© β£ (πβπ€) E (πβπ§)}) β V) |
22 | 20, 21 | eqeltrrid 2839 |
. . . . . . . . . . 11
β’ ((π΄ Γ π΄) β V β ({β¨π€, π§β© β£ (πβπ€) E (πβπ§)} β© (π΄ Γ π΄)) β V) |
23 | | weeq1 5665 |
. . . . . . . . . . . 12
β’ (π₯ = ({β¨π€, π§β© β£ (πβπ€) E (πβπ§)} β© (π΄ Γ π΄)) β (π₯ We π΄ β ({β¨π€, π§β© β£ (πβπ€) E (πβπ§)} β© (π΄ Γ π΄)) We π΄)) |
24 | 23 | spcegv 3588 |
. . . . . . . . . . 11
β’
(({β¨π€, π§β© β£ (πβπ€) E (πβπ§)} β© (π΄ Γ π΄)) β V β (({β¨π€, π§β© β£ (πβπ€) E (πβπ§)} β© (π΄ Γ π΄)) We π΄ β βπ₯ π₯ We π΄)) |
25 | 18, 19, 22, 24 | 4syl 19 |
. . . . . . . . . 10
β’ (π΄ βΌ π¦ β (({β¨π€, π§β© β£ (πβπ€) E (πβπ§)} β© (π΄ Γ π΄)) We π΄ β βπ₯ π₯ We π΄)) |
26 | 16, 25 | biimtrid 241 |
. . . . . . . . 9
β’ (π΄ βΌ π¦ β ({β¨π€, π§β© β£ (πβπ€) E (πβπ§)} We π΄ β βπ₯ π₯ We π΄)) |
27 | 15, 26 | sylan9r 510 |
. . . . . . . 8
β’ ((π΄ βΌ π¦ β§ π:π΄β1-1βπ¦) β ( E We ran π β βπ₯ π₯ We π΄)) |
28 | 11, 27 | syld 47 |
. . . . . . 7
β’ ((π΄ βΌ π¦ β§ π:π΄β1-1βπ¦) β (π¦ β On β βπ₯ π₯ We π΄)) |
29 | 28 | impancom 453 |
. . . . . 6
β’ ((π΄ βΌ π¦ β§ π¦ β On) β (π:π΄β1-1βπ¦ β βπ₯ π₯ We π΄)) |
30 | 29 | exlimdv 1937 |
. . . . 5
β’ ((π΄ βΌ π¦ β§ π¦ β On) β (βπ π:π΄β1-1βπ¦ β βπ₯ π₯ We π΄)) |
31 | 2, 30 | biimtrid 241 |
. . . 4
β’ ((π΄ βΌ π¦ β§ π¦ β On) β (π΄ βΌ π¦ β βπ₯ π₯ We π΄)) |
32 | 31 | ex 414 |
. . 3
β’ (π΄ βΌ π¦ β (π¦ β On β (π΄ βΌ π¦ β βπ₯ π₯ We π΄))) |
33 | 32 | pm2.43b 55 |
. 2
β’ (π¦ β On β (π΄ βΌ π¦ β βπ₯ π₯ We π΄)) |
34 | 33 | rexlimiv 3149 |
1
β’
(βπ¦ β On
π΄ βΌ π¦ β βπ₯ π₯ We π΄) |