Step | Hyp | Ref
| Expression |
1 | | vex 3448 |
. . . . 5
β’ π₯ β V |
2 | | vex 3448 |
. . . . 5
β’ π¦ β V |
3 | 1, 2 | brcnv 5839 |
. . . 4
β’ (π₯β‘(1st βΎ I )π¦ β π¦(1st βΎ I )π₯) |
4 | 1 | brresi 5947 |
. . . 4
β’ (π¦(1st βΎ I )π₯ β (π¦ β I β§ π¦1st π₯)) |
5 | | 19.42v 1958 |
. . . . . 6
β’
(βπ§((1st βπ¦) = π₯ β§ π¦ = β¨π§, π§β©) β ((1st βπ¦) = π₯ β§ βπ§ π¦ = β¨π§, π§β©)) |
6 | | vex 3448 |
. . . . . . . . . 10
β’ π§ β V |
7 | 6, 6 | op1std 7932 |
. . . . . . . . 9
β’ (π¦ = β¨π§, π§β© β (1st βπ¦) = π§) |
8 | 7 | eqeq1d 2735 |
. . . . . . . 8
β’ (π¦ = β¨π§, π§β© β ((1st βπ¦) = π₯ β π§ = π₯)) |
9 | 8 | pm5.32ri 577 |
. . . . . . 7
β’
(((1st βπ¦) = π₯ β§ π¦ = β¨π§, π§β©) β (π§ = π₯ β§ π¦ = β¨π§, π§β©)) |
10 | 9 | exbii 1851 |
. . . . . 6
β’
(βπ§((1st βπ¦) = π₯ β§ π¦ = β¨π§, π§β©) β βπ§(π§ = π₯ β§ π¦ = β¨π§, π§β©)) |
11 | | fo1st 7942 |
. . . . . . . . 9
β’
1st :VβontoβV |
12 | | fofn 6759 |
. . . . . . . . 9
β’
(1st :VβontoβV β 1st Fn V) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . 8
β’
1st Fn V |
14 | | fnbrfvb 6896 |
. . . . . . . 8
β’
((1st Fn V β§ π¦ β V) β ((1st
βπ¦) = π₯ β π¦1st π₯)) |
15 | 13, 2, 14 | mp2an 691 |
. . . . . . 7
β’
((1st βπ¦) = π₯ β π¦1st π₯) |
16 | | df-id 5532 |
. . . . . . . . 9
β’ I =
{β¨π§, π‘β© β£ π§ = π‘} |
17 | 16 | eleq2i 2826 |
. . . . . . . 8
β’ (π¦ β I β π¦ β {β¨π§, π‘β© β£ π§ = π‘}) |
18 | | elopab 5485 |
. . . . . . . 8
β’ (π¦ β {β¨π§, π‘β© β£ π§ = π‘} β βπ§βπ‘(π¦ = β¨π§, π‘β© β§ π§ = π‘)) |
19 | | ancom 462 |
. . . . . . . . . . . 12
β’ ((π¦ = β¨π§, π‘β© β§ π§ = π‘) β (π§ = π‘ β§ π¦ = β¨π§, π‘β©)) |
20 | | equcom 2022 |
. . . . . . . . . . . . 13
β’ (π§ = π‘ β π‘ = π§) |
21 | 20 | anbi1i 625 |
. . . . . . . . . . . 12
β’ ((π§ = π‘ β§ π¦ = β¨π§, π‘β©) β (π‘ = π§ β§ π¦ = β¨π§, π‘β©)) |
22 | | opeq2 4832 |
. . . . . . . . . . . . . 14
β’ (π‘ = π§ β β¨π§, π‘β© = β¨π§, π§β©) |
23 | 22 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ (π‘ = π§ β (π¦ = β¨π§, π‘β© β π¦ = β¨π§, π§β©)) |
24 | 23 | pm5.32i 576 |
. . . . . . . . . . . 12
β’ ((π‘ = π§ β§ π¦ = β¨π§, π‘β©) β (π‘ = π§ β§ π¦ = β¨π§, π§β©)) |
25 | 19, 21, 24 | 3bitri 297 |
. . . . . . . . . . 11
β’ ((π¦ = β¨π§, π‘β© β§ π§ = π‘) β (π‘ = π§ β§ π¦ = β¨π§, π§β©)) |
26 | 25 | exbii 1851 |
. . . . . . . . . 10
β’
(βπ‘(π¦ = β¨π§, π‘β© β§ π§ = π‘) β βπ‘(π‘ = π§ β§ π¦ = β¨π§, π§β©)) |
27 | | biidd 262 |
. . . . . . . . . . 11
β’ (π‘ = π§ β (π¦ = β¨π§, π§β© β π¦ = β¨π§, π§β©)) |
28 | 27 | equsexvw 2009 |
. . . . . . . . . 10
β’
(βπ‘(π‘ = π§ β§ π¦ = β¨π§, π§β©) β π¦ = β¨π§, π§β©) |
29 | 26, 28 | bitri 275 |
. . . . . . . . 9
β’
(βπ‘(π¦ = β¨π§, π‘β© β§ π§ = π‘) β π¦ = β¨π§, π§β©) |
30 | 29 | exbii 1851 |
. . . . . . . 8
β’
(βπ§βπ‘(π¦ = β¨π§, π‘β© β§ π§ = π‘) β βπ§ π¦ = β¨π§, π§β©) |
31 | 17, 18, 30 | 3bitrri 298 |
. . . . . . 7
β’
(βπ§ π¦ = β¨π§, π§β© β π¦ β I ) |
32 | 15, 31 | anbi12ci 629 |
. . . . . 6
β’
(((1st βπ¦) = π₯ β§ βπ§ π¦ = β¨π§, π§β©) β (π¦ β I β§ π¦1st π₯)) |
33 | 5, 10, 32 | 3bitr3ri 302 |
. . . . 5
β’ ((π¦ β I β§ π¦1st π₯) β βπ§(π§ = π₯ β§ π¦ = β¨π§, π§β©)) |
34 | | id 22 |
. . . . . . . 8
β’ (π§ = π₯ β π§ = π₯) |
35 | 34, 34 | opeq12d 4839 |
. . . . . . 7
β’ (π§ = π₯ β β¨π§, π§β© = β¨π₯, π₯β©) |
36 | 35 | eqeq2d 2744 |
. . . . . 6
β’ (π§ = π₯ β (π¦ = β¨π§, π§β© β π¦ = β¨π₯, π₯β©)) |
37 | 36 | equsexvw 2009 |
. . . . 5
β’
(βπ§(π§ = π₯ β§ π¦ = β¨π§, π§β©) β π¦ = β¨π₯, π₯β©) |
38 | 33, 37 | bitri 275 |
. . . 4
β’ ((π¦ β I β§ π¦1st π₯) β π¦ = β¨π₯, π₯β©) |
39 | 3, 4, 38 | 3bitri 297 |
. . 3
β’ (π₯β‘(1st βΎ I )π¦ β π¦ = β¨π₯, π₯β©) |
40 | 39 | opabbii 5173 |
. 2
β’
{β¨π₯, π¦β© β£ π₯β‘(1st βΎ I )π¦} = {β¨π₯, π¦β© β£ π¦ = β¨π₯, π₯β©} |
41 | | relcnv 6057 |
. . 3
β’ Rel β‘(1st βΎ I ) |
42 | | dfrel4v 6143 |
. . 3
β’ (Rel
β‘(1st βΎ I ) β
β‘(1st βΎ I ) =
{β¨π₯, π¦β© β£ π₯β‘(1st βΎ I )π¦}) |
43 | 41, 42 | mpbi 229 |
. 2
β’ β‘(1st βΎ I ) = {β¨π₯, π¦β© β£ π₯β‘(1st βΎ I )π¦} |
44 | | mptv 5222 |
. 2
β’ (π₯ β V β¦ β¨π₯, π₯β©) = {β¨π₯, π¦β© β£ π¦ = β¨π₯, π₯β©} |
45 | 40, 43, 44 | 3eqtr4i 2771 |
1
β’ β‘(1st βΎ I ) = (π₯ β V β¦ β¨π₯, π₯β©) |