Step | Hyp | Ref
| Expression |
1 | | efgrelexlem.1 |
. . 3
β’ πΏ = {β¨π, πβ© β£ βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0)} |
2 | 1 | bropaex12 5765 |
. 2
β’ (π΄πΏπ΅ β (π΄ β V β§ π΅ β V)) |
3 | | n0i 4332 |
. . . . . 6
β’ (π β (β‘π β {π΄}) β Β¬ (β‘π β {π΄}) = β
) |
4 | | snprc 4720 |
. . . . . . . 8
β’ (Β¬
π΄ β V β {π΄} = β
) |
5 | | imaeq2 6053 |
. . . . . . . 8
β’ ({π΄} = β
β (β‘π β {π΄}) = (β‘π β β
)) |
6 | 4, 5 | sylbi 216 |
. . . . . . 7
β’ (Β¬
π΄ β V β (β‘π β {π΄}) = (β‘π β β
)) |
7 | | ima0 6073 |
. . . . . . 7
β’ (β‘π β β
) = β
|
8 | 6, 7 | eqtrdi 2788 |
. . . . . 6
β’ (Β¬
π΄ β V β (β‘π β {π΄}) = β
) |
9 | 3, 8 | nsyl2 141 |
. . . . 5
β’ (π β (β‘π β {π΄}) β π΄ β V) |
10 | | n0i 4332 |
. . . . . 6
β’ (π β (β‘π β {π΅}) β Β¬ (β‘π β {π΅}) = β
) |
11 | | snprc 4720 |
. . . . . . . 8
β’ (Β¬
π΅ β V β {π΅} = β
) |
12 | | imaeq2 6053 |
. . . . . . . 8
β’ ({π΅} = β
β (β‘π β {π΅}) = (β‘π β β
)) |
13 | 11, 12 | sylbi 216 |
. . . . . . 7
β’ (Β¬
π΅ β V β (β‘π β {π΅}) = (β‘π β β
)) |
14 | 13, 7 | eqtrdi 2788 |
. . . . . 6
β’ (Β¬
π΅ β V β (β‘π β {π΅}) = β
) |
15 | 10, 14 | nsyl2 141 |
. . . . 5
β’ (π β (β‘π β {π΅}) β π΅ β V) |
16 | 9, 15 | anim12i 613 |
. . . 4
β’ ((π β (β‘π β {π΄}) β§ π β (β‘π β {π΅})) β (π΄ β V β§ π΅ β V)) |
17 | 16 | a1d 25 |
. . 3
β’ ((π β (β‘π β {π΄}) β§ π β (β‘π β {π΅})) β ((πβ0) = (πβ0) β (π΄ β V β§ π΅ β V))) |
18 | 17 | rexlimivv 3199 |
. 2
β’
(βπ β
(β‘π β {π΄})βπ β (β‘π β {π΅})(πβ0) = (πβ0) β (π΄ β V β§ π΅ β V)) |
19 | | fveq1 6887 |
. . . . . 6
β’ (π = π β (πβ0) = (πβ0)) |
20 | 19 | eqeq1d 2734 |
. . . . 5
β’ (π = π β ((πβ0) = (πβ0) β (πβ0) = (πβ0))) |
21 | | fveq1 6887 |
. . . . . 6
β’ (π = π β (πβ0) = (πβ0)) |
22 | 21 | eqeq2d 2743 |
. . . . 5
β’ (π = π β ((πβ0) = (πβ0) β (πβ0) = (πβ0))) |
23 | 20, 22 | cbvrex2vw 3239 |
. . . 4
β’
(βπ β
(β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0) β βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0)) |
24 | | sneq 4637 |
. . . . . 6
β’ (π = π΄ β {π} = {π΄}) |
25 | 24 | imaeq2d 6057 |
. . . . 5
β’ (π = π΄ β (β‘π β {π}) = (β‘π β {π΄})) |
26 | 25 | rexeqdv 3326 |
. . . 4
β’ (π = π΄ β (βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0) β βπ β (β‘π β {π΄})βπ β (β‘π β {π})(πβ0) = (πβ0))) |
27 | 23, 26 | bitrid 282 |
. . 3
β’ (π = π΄ β (βπ β (β‘π β {π})βπ β (β‘π β {π})(πβ0) = (πβ0) β βπ β (β‘π β {π΄})βπ β (β‘π β {π})(πβ0) = (πβ0))) |
28 | | sneq 4637 |
. . . . . 6
β’ (π = π΅ β {π} = {π΅}) |
29 | 28 | imaeq2d 6057 |
. . . . 5
β’ (π = π΅ β (β‘π β {π}) = (β‘π β {π΅})) |
30 | 29 | rexeqdv 3326 |
. . . 4
β’ (π = π΅ β (βπ β (β‘π β {π})(πβ0) = (πβ0) β βπ β (β‘π β {π΅})(πβ0) = (πβ0))) |
31 | 30 | rexbidv 3178 |
. . 3
β’ (π = π΅ β (βπ β (β‘π β {π΄})βπ β (β‘π β {π})(πβ0) = (πβ0) β βπ β (β‘π β {π΄})βπ β (β‘π β {π΅})(πβ0) = (πβ0))) |
32 | 27, 31, 1 | brabg 5538 |
. 2
β’ ((π΄ β V β§ π΅ β V) β (π΄πΏπ΅ β βπ β (β‘π β {π΄})βπ β (β‘π β {π΅})(πβ0) = (πβ0))) |
33 | 2, 18, 32 | pm5.21nii 379 |
1
β’ (π΄πΏπ΅ β βπ β (β‘π β {π΄})βπ β (β‘π β {π΅})(πβ0) = (πβ0)) |