Step | Hyp | Ref
| Expression |
1 | | snnzg 4736 |
. . 3
ā¢ (š“ ā š ā {š“} ā ā
) |
2 | | fo2ndres 7949 |
. . 3
ā¢ ({š“} ā ā
ā
(2nd ā¾ ({š“} Ć šµ)):({š“} Ć šµ)āontoāšµ) |
3 | 1, 2 | syl 17 |
. 2
ā¢ (š“ ā š ā (2nd ā¾ ({š“} Ć šµ)):({š“} Ć šµ)āontoāšµ) |
4 | | moeq 3666 |
. . . . . 6
ā¢
ā*š„ š„ = āØš“, š¦ā© |
5 | 4 | moani 2548 |
. . . . 5
ā¢
ā*š„(š¦ ā šµ ā§ š„ = āØš“, š¦ā©) |
6 | | vex 3448 |
. . . . . . . 8
ā¢ š¦ ā V |
7 | 6 | brresi 5947 |
. . . . . . 7
ā¢ (š„(2nd ā¾ ({š“} Ć šµ))š¦ ā (š„ ā ({š“} Ć šµ) ā§ š„2nd š¦)) |
8 | | fo2nd 7943 |
. . . . . . . . . . 11
ā¢
2nd :VāontoāV |
9 | | fofn 6759 |
. . . . . . . . . . 11
ā¢
(2nd :VāontoāV ā 2nd Fn V) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . 10
ā¢
2nd Fn V |
11 | | vex 3448 |
. . . . . . . . . 10
ā¢ š„ ā V |
12 | | fnbrfvb 6896 |
. . . . . . . . . 10
ā¢
((2nd Fn V ā§ š„ ā V) ā ((2nd
āš„) = š¦ ā š„2nd š¦)) |
13 | 10, 11, 12 | mp2an 691 |
. . . . . . . . 9
ā¢
((2nd āš„) = š¦ ā š„2nd š¦) |
14 | 13 | anbi2i 624 |
. . . . . . . 8
ā¢ ((š„ ā ({š“} Ć šµ) ā§ (2nd āš„) = š¦) ā (š„ ā ({š“} Ć šµ) ā§ š„2nd š¦)) |
15 | | elxp7 7957 |
. . . . . . . . . . 11
ā¢ (š„ ā ({š“} Ć šµ) ā (š„ ā (V Ć V) ā§ ((1st
āš„) ā {š“} ā§ (2nd
āš„) ā šµ))) |
16 | | eleq1 2822 |
. . . . . . . . . . . . . . 15
ā¢
((2nd āš„) = š¦ ā ((2nd āš„) ā šµ ā š¦ ā šµ)) |
17 | 16 | biimpac 480 |
. . . . . . . . . . . . . 14
ā¢
(((2nd āš„) ā šµ ā§ (2nd āš„) = š¦) ā š¦ ā šµ) |
18 | 17 | adantll 713 |
. . . . . . . . . . . . 13
ā¢
((((1st āš„) ā {š“} ā§ (2nd āš„) ā šµ) ā§ (2nd āš„) = š¦) ā š¦ ā šµ) |
19 | 18 | adantll 713 |
. . . . . . . . . . . 12
ā¢ (((š„ ā (V Ć V) ā§
((1st āš„)
ā {š“} ā§
(2nd āš„)
ā šµ)) ā§
(2nd āš„) =
š¦) ā š¦ ā šµ) |
20 | | elsni 4604 |
. . . . . . . . . . . . . 14
ā¢
((1st āš„) ā {š“} ā (1st āš„) = š“) |
21 | | eqopi 7958 |
. . . . . . . . . . . . . . 15
ā¢ ((š„ ā (V Ć V) ā§
((1st āš„)
= š“ ā§ (2nd
āš„) = š¦)) ā š„ = āØš“, š¦ā©) |
22 | 21 | anassrs 469 |
. . . . . . . . . . . . . 14
ā¢ (((š„ ā (V Ć V) ā§
(1st āš„) =
š“) ā§ (2nd
āš„) = š¦) ā š„ = āØš“, š¦ā©) |
23 | 20, 22 | sylanl2 680 |
. . . . . . . . . . . . 13
ā¢ (((š„ ā (V Ć V) ā§
(1st āš„)
ā {š“}) ā§
(2nd āš„) =
š¦) ā š„ = āØš“, š¦ā©) |
24 | 23 | adantlrr 720 |
. . . . . . . . . . . 12
ā¢ (((š„ ā (V Ć V) ā§
((1st āš„)
ā {š“} ā§
(2nd āš„)
ā šµ)) ā§
(2nd āš„) =
š¦) ā š„ = āØš“, š¦ā©) |
25 | 19, 24 | jca 513 |
. . . . . . . . . . 11
ā¢ (((š„ ā (V Ć V) ā§
((1st āš„)
ā {š“} ā§
(2nd āš„)
ā šµ)) ā§
(2nd āš„) =
š¦) ā (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) |
26 | 15, 25 | sylanb 582 |
. . . . . . . . . 10
ā¢ ((š„ ā ({š“} Ć šµ) ā§ (2nd āš„) = š¦) ā (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) |
27 | 26 | adantl 483 |
. . . . . . . . 9
ā¢ ((š“ ā š ā§ (š„ ā ({š“} Ć šµ) ā§ (2nd āš„) = š¦)) ā (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) |
28 | | simprr 772 |
. . . . . . . . . . 11
ā¢ ((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā š„ = āØš“, š¦ā©) |
29 | | snidg 4621 |
. . . . . . . . . . . . 13
ā¢ (š“ ā š ā š“ ā {š“}) |
30 | 29 | adantr 482 |
. . . . . . . . . . . 12
ā¢ ((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā š“ ā {š“}) |
31 | | simprl 770 |
. . . . . . . . . . . 12
ā¢ ((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā š¦ ā šµ) |
32 | 30, 31 | opelxpd 5672 |
. . . . . . . . . . 11
ā¢ ((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā āØš“, š¦ā© ā ({š“} Ć šµ)) |
33 | 28, 32 | eqeltrd 2834 |
. . . . . . . . . 10
ā¢ ((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā š„ ā ({š“} Ć šµ)) |
34 | | fveq2 6843 |
. . . . . . . . . . . 12
ā¢ (š„ = āØš“, š¦ā© ā (2nd āš„) = (2nd
āāØš“, š¦ā©)) |
35 | | op2ndg 7935 |
. . . . . . . . . . . . 13
ā¢ ((š“ ā š ā§ š¦ ā V) ā (2nd
āāØš“, š¦ā©) = š¦) |
36 | 35 | elvd 3451 |
. . . . . . . . . . . 12
ā¢ (š“ ā š ā (2nd āāØš“, š¦ā©) = š¦) |
37 | 34, 36 | sylan9eqr 2795 |
. . . . . . . . . . 11
ā¢ ((š“ ā š ā§ š„ = āØš“, š¦ā©) ā (2nd āš„) = š¦) |
38 | 37 | adantrl 715 |
. . . . . . . . . 10
ā¢ ((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā (2nd āš„) = š¦) |
39 | 33, 38 | jca 513 |
. . . . . . . . 9
ā¢ ((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā (š„ ā ({š“} Ć šµ) ā§ (2nd āš„) = š¦)) |
40 | 27, 39 | impbida 800 |
. . . . . . . 8
ā¢ (š“ ā š ā ((š„ ā ({š“} Ć šµ) ā§ (2nd āš„) = š¦) ā (š¦ ā šµ ā§ š„ = āØš“, š¦ā©))) |
41 | 14, 40 | bitr3id 285 |
. . . . . . 7
ā¢ (š“ ā š ā ((š„ ā ({š“} Ć šµ) ā§ š„2nd š¦) ā (š¦ ā šµ ā§ š„ = āØš“, š¦ā©))) |
42 | 7, 41 | bitrid 283 |
. . . . . 6
ā¢ (š“ ā š ā (š„(2nd ā¾ ({š“} Ć šµ))š¦ ā (š¦ ā šµ ā§ š„ = āØš“, š¦ā©))) |
43 | 42 | mobidv 2544 |
. . . . 5
ā¢ (š“ ā š ā (ā*š„ š„(2nd ā¾ ({š“} Ć šµ))š¦ ā ā*š„(š¦ ā šµ ā§ š„ = āØš“, š¦ā©))) |
44 | 5, 43 | mpbiri 258 |
. . . 4
ā¢ (š“ ā š ā ā*š„ š„(2nd ā¾ ({š“} Ć šµ))š¦) |
45 | 44 | alrimiv 1931 |
. . 3
ā¢ (š“ ā š ā āš¦ā*š„ š„(2nd ā¾ ({š“} Ć šµ))š¦) |
46 | | funcnv2 6570 |
. . 3
ā¢ (Fun
ā”(2nd ā¾ ({š“} Ć šµ)) ā āš¦ā*š„ š„(2nd ā¾ ({š“} Ć šµ))š¦) |
47 | 45, 46 | sylibr 233 |
. 2
ā¢ (š“ ā š ā Fun ā”(2nd ā¾ ({š“} Ć šµ))) |
48 | | dff1o3 6791 |
. 2
ā¢
((2nd ā¾ ({š“} Ć šµ)):({š“} Ć šµ)ā1-1-ontoāšµ ā ((2nd ā¾
({š“} Ć šµ)):({š“} Ć šµ)āontoāšµ ā§ Fun ā”(2nd ā¾ ({š“} Ć šµ)))) |
49 | 3, 47, 48 | sylanbrc 584 |
1
ā¢ (š“ ā š ā (2nd ā¾ ({š“} Ć šµ)):({š“} Ć šµ)ā1-1-ontoāšµ) |