Step | Hyp | Ref
| Expression |
1 | | ima0 6076 |
. . . 4
ā¢
(2nd ā ā
) = ā
|
2 | | xpeq2 5697 |
. . . . . 6
⢠(šµ = ā
ā (š“ Ć šµ) = (š“ Ć ā
)) |
3 | | xp0 6157 |
. . . . . 6
⢠(š“ Ć ā
) =
ā
|
4 | 2, 3 | eqtrdi 2787 |
. . . . 5
⢠(šµ = ā
ā (š“ Ć šµ) = ā
) |
5 | 4 | imaeq2d 6059 |
. . . 4
⢠(šµ = ā
ā
(2nd ā (š“
Ć šµ)) =
(2nd ā ā
)) |
6 | | id 22 |
. . . 4
⢠(šµ = ā
ā šµ = ā
) |
7 | 1, 5, 6 | 3eqtr4a 2797 |
. . 3
⢠(šµ = ā
ā
(2nd ā (š“
Ć šµ)) = šµ) |
8 | 7 | adantl 481 |
. 2
⢠((š“ ā ā
ā§ šµ = ā
) ā
(2nd ā (š“
Ć šµ)) = šµ) |
9 | | xpnz 6158 |
. . . . 5
⢠((š“ ā ā
ā§ šµ ā ā
) ā (š“ Ć šµ) ā ā
) |
10 | | fo2nd 7999 |
. . . . . . 7
ā¢
2nd :VāontoāV |
11 | | fofn 6807 |
. . . . . . 7
ā¢
(2nd :VāontoāV ā 2nd Fn V) |
12 | 10, 11 | mp1i 13 |
. . . . . 6
⢠((š“ Ć šµ) ā ā
ā 2nd Fn
V) |
13 | | ssv 4006 |
. . . . . . 7
⢠(š“ Ć šµ) ā V |
14 | 13 | a1i 11 |
. . . . . 6
⢠((š“ Ć šµ) ā ā
ā (š“ Ć šµ) ā V) |
15 | 12, 14 | fvelimabd 6965 |
. . . . 5
⢠((š“ Ć šµ) ā ā
ā (š¦ ā (2nd ā (š“ Ć šµ)) ā āš ā (š“ Ć šµ)(2nd āš) = š¦)) |
16 | 9, 15 | sylbi 216 |
. . . 4
⢠((š“ ā ā
ā§ šµ ā ā
) ā (š¦ ā (2nd ā
(š“ Ć šµ)) ā āš ā (š“ Ć šµ)(2nd āš) = š¦)) |
17 | | simpr 484 |
. . . . . . 7
⢠((((š“ ā ā
ā§ šµ ā ā
) ā§ š ā (š“ Ć šµ)) ā§ (2nd āš) = š¦) ā (2nd āš) = š¦) |
18 | | xp2nd 8011 |
. . . . . . . 8
⢠(š ā (š“ Ć šµ) ā (2nd āš) ā šµ) |
19 | 18 | ad2antlr 724 |
. . . . . . 7
⢠((((š“ ā ā
ā§ šµ ā ā
) ā§ š ā (š“ Ć šµ)) ā§ (2nd āš) = š¦) ā (2nd āš) ā šµ) |
20 | 17, 19 | eqeltrrd 2833 |
. . . . . 6
⢠((((š“ ā ā
ā§ šµ ā ā
) ā§ š ā (š“ Ć šµ)) ā§ (2nd āš) = š¦) ā š¦ ā šµ) |
21 | 20 | r19.29an 3157 |
. . . . 5
⢠(((š“ ā ā
ā§ šµ ā ā
) ā§
āš ā (š“ Ć šµ)(2nd āš) = š¦) ā š¦ ā šµ) |
22 | | n0 4346 |
. . . . . . . 8
⢠(š“ ā ā
ā
āš„ š„ ā š“) |
23 | 22 | biimpi 215 |
. . . . . . 7
⢠(š“ ā ā
ā
āš„ š„ ā š“) |
24 | 23 | ad2antrr 723 |
. . . . . 6
⢠(((š“ ā ā
ā§ šµ ā ā
) ā§ š¦ ā šµ) ā āš„ š„ ā š“) |
25 | | opelxpi 5713 |
. . . . . . . . 9
⢠((š„ ā š“ ā§ š¦ ā šµ) ā āØš„, š¦ā© ā (š“ Ć šµ)) |
26 | 25 | ancoms 458 |
. . . . . . . 8
⢠((š¦ ā šµ ā§ š„ ā š“) ā āØš„, š¦ā© ā (š“ Ć šµ)) |
27 | 26 | adantll 711 |
. . . . . . 7
⢠((((š“ ā ā
ā§ šµ ā ā
) ā§ š¦ ā šµ) ā§ š„ ā š“) ā āØš„, š¦ā© ā (š“ Ć šµ)) |
28 | | fveqeq2 6900 |
. . . . . . . 8
⢠(š = āØš„, š¦ā© ā ((2nd āš) = š¦ ā (2nd āāØš„, š¦ā©) = š¦)) |
29 | 28 | adantl 481 |
. . . . . . 7
ā¢
(((((š“ ā ā
ā§ šµ ā ā
) ā§
š¦ ā šµ) ā§ š„ ā š“) ā§ š = āØš„, š¦ā©) ā ((2nd āš) = š¦ ā (2nd āāØš„, š¦ā©) = š¦)) |
30 | | vex 3477 |
. . . . . . . . 9
⢠š„ ā V |
31 | | vex 3477 |
. . . . . . . . 9
⢠š¦ ā V |
32 | 30, 31 | op2nd 7987 |
. . . . . . . 8
ā¢
(2nd āāØš„, š¦ā©) = š¦ |
33 | 32 | a1i 11 |
. . . . . . 7
⢠((((š“ ā ā
ā§ šµ ā ā
) ā§ š¦ ā šµ) ā§ š„ ā š“) ā (2nd āāØš„, š¦ā©) = š¦) |
34 | 27, 29, 33 | rspcedvd 3614 |
. . . . . 6
⢠((((š“ ā ā
ā§ šµ ā ā
) ā§ š¦ ā šµ) ā§ š„ ā š“) ā āš ā (š“ Ć šµ)(2nd āš) = š¦) |
35 | 24, 34 | exlimddv 1937 |
. . . . 5
⢠(((š“ ā ā
ā§ šµ ā ā
) ā§ š¦ ā šµ) ā āš ā (š“ Ć šµ)(2nd āš) = š¦) |
36 | 21, 35 | impbida 798 |
. . . 4
⢠((š“ ā ā
ā§ šµ ā ā
) ā
(āš ā (š“ Ć šµ)(2nd āš) = š¦ ā š¦ ā šµ)) |
37 | 16, 36 | bitrd 279 |
. . 3
⢠((š“ ā ā
ā§ šµ ā ā
) ā (š¦ ā (2nd ā
(š“ Ć šµ)) ā š¦ ā šµ)) |
38 | 37 | eqrdv 2729 |
. 2
⢠((š“ ā ā
ā§ šµ ā ā
) ā
(2nd ā (š“
Ć šµ)) = šµ) |
39 | 8, 38 | pm2.61dane 3028 |
1
⢠(š“ ā ā
ā
(2nd ā (š“
Ć šµ)) = šµ) |