Step | Hyp | Ref
| Expression |
1 | | snmg 3712 |
. . 3
⢠(š“ ā š ā āš„ š„ ā {š“}) |
2 | | fo2ndresm 6166 |
. . 3
ā¢
(āš„ š„ ā {š“} ā (2nd ā¾ ({š“} Ć šµ)):({š“} Ć šµ)āontoāšµ) |
3 | 1, 2 | syl 14 |
. 2
⢠(š“ ā š ā (2nd ā¾ ({š“} Ć šµ)):({š“} Ć šµ)āontoāšµ) |
4 | | moeq 2914 |
. . . . . 6
ā¢
ā*š„ š„ = āØš“, š¦ā© |
5 | 4 | moani 2096 |
. . . . 5
ā¢
ā*š„(š¦ ā šµ ā§ š„ = āØš“, š¦ā©) |
6 | | vex 2742 |
. . . . . . . 8
⢠š¦ ā V |
7 | 6 | brres 4915 |
. . . . . . 7
⢠(š„(2nd ā¾ ({š“} Ć šµ))š¦ ā (š„2nd š¦ ā§ š„ ā ({š“} Ć šµ))) |
8 | | fo2nd 6162 |
. . . . . . . . . . 11
ā¢
2nd :VāontoāV |
9 | | fofn 5442 |
. . . . . . . . . . 11
ā¢
(2nd :VāontoāV ā 2nd Fn V) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . 10
ā¢
2nd Fn V |
11 | | vex 2742 |
. . . . . . . . . 10
⢠š„ ā V |
12 | | fnbrfvb 5559 |
. . . . . . . . . 10
ā¢
((2nd Fn V ā§ š„ ā V) ā ((2nd
āš„) = š¦ ā š„2nd š¦)) |
13 | 10, 11, 12 | mp2an 426 |
. . . . . . . . 9
ā¢
((2nd āš„) = š¦ ā š„2nd š¦) |
14 | 13 | anbi1i 458 |
. . . . . . . 8
ā¢
(((2nd āš„) = š¦ ā§ š„ ā ({š“} Ć šµ)) ā (š„2nd š¦ ā§ š„ ā ({š“} Ć šµ))) |
15 | | elxp7 6174 |
. . . . . . . . . . 11
⢠(š„ ā ({š“} Ć šµ) ā (š„ ā (V Ć V) ā§ ((1st
āš„) ā {š“} ā§ (2nd
āš„) ā šµ))) |
16 | | eleq1 2240 |
. . . . . . . . . . . . . . 15
ā¢
((2nd āš„) = š¦ ā ((2nd āš„) ā šµ ā š¦ ā šµ)) |
17 | 16 | biimpa 296 |
. . . . . . . . . . . . . 14
ā¢
(((2nd āš„) = š¦ ā§ (2nd āš„) ā šµ) ā š¦ ā šµ) |
18 | 17 | adantrl 478 |
. . . . . . . . . . . . 13
ā¢
(((2nd āš„) = š¦ ā§ ((1st āš„) ā {š“} ā§ (2nd āš„) ā šµ)) ā š¦ ā šµ) |
19 | 18 | adantrl 478 |
. . . . . . . . . . . 12
ā¢
(((2nd āš„) = š¦ ā§ (š„ ā (V Ć V) ā§ ((1st
āš„) ā {š“} ā§ (2nd
āš„) ā šµ))) ā š¦ ā šµ) |
20 | | elsni 3612 |
. . . . . . . . . . . . . 14
ā¢
((1st āš„) ā {š“} ā (1st āš„) = š“) |
21 | | eqopi 6176 |
. . . . . . . . . . . . . . . 16
⢠((š„ ā (V Ć V) ā§
((1st āš„)
= š“ ā§ (2nd
āš„) = š¦)) ā š„ = āØš“, š¦ā©) |
22 | 21 | ancom2s 566 |
. . . . . . . . . . . . . . 15
⢠((š„ ā (V Ć V) ā§
((2nd āš„)
= š¦ ā§ (1st
āš„) = š“)) ā š„ = āØš“, š¦ā©) |
23 | 22 | an12s 565 |
. . . . . . . . . . . . . 14
ā¢
(((2nd āš„) = š¦ ā§ (š„ ā (V Ć V) ā§ (1st
āš„) = š“)) ā š„ = āØš“, š¦ā©) |
24 | 20, 23 | sylanr2 405 |
. . . . . . . . . . . . 13
ā¢
(((2nd āš„) = š¦ ā§ (š„ ā (V Ć V) ā§ (1st
āš„) ā {š“})) ā š„ = āØš“, š¦ā©) |
25 | 24 | adantrrr 487 |
. . . . . . . . . . . 12
ā¢
(((2nd āš„) = š¦ ā§ (š„ ā (V Ć V) ā§ ((1st
āš„) ā {š“} ā§ (2nd
āš„) ā šµ))) ā š„ = āØš“, š¦ā©) |
26 | 19, 25 | jca 306 |
. . . . . . . . . . 11
ā¢
(((2nd āš„) = š¦ ā§ (š„ ā (V Ć V) ā§ ((1st
āš„) ā {š“} ā§ (2nd
āš„) ā šµ))) ā (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) |
27 | 15, 26 | sylan2b 287 |
. . . . . . . . . 10
ā¢
(((2nd āš„) = š¦ ā§ š„ ā ({š“} Ć šµ)) ā (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) |
28 | 27 | adantl 277 |
. . . . . . . . 9
⢠((š“ ā š ā§ ((2nd āš„) = š¦ ā§ š„ ā ({š“} Ć šµ))) ā (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) |
29 | | fveq2 5517 |
. . . . . . . . . . . 12
⢠(š„ = āØš“, š¦ā© ā (2nd āš„) = (2nd
āāØš“, š¦ā©)) |
30 | | op2ndg 6155 |
. . . . . . . . . . . . 13
⢠((š“ ā š ā§ š¦ ā V) ā (2nd
āāØš“, š¦ā©) = š¦) |
31 | 6, 30 | mpan2 425 |
. . . . . . . . . . . 12
⢠(š“ ā š ā (2nd āāØš“, š¦ā©) = š¦) |
32 | 29, 31 | sylan9eqr 2232 |
. . . . . . . . . . 11
⢠((š“ ā š ā§ š„ = āØš“, š¦ā©) ā (2nd āš„) = š¦) |
33 | 32 | adantrl 478 |
. . . . . . . . . 10
⢠((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā (2nd āš„) = š¦) |
34 | | simprr 531 |
. . . . . . . . . . 11
⢠((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā š„ = āØš“, š¦ā©) |
35 | | snidg 3623 |
. . . . . . . . . . . . 13
⢠(š“ ā š ā š“ ā {š“}) |
36 | 35 | adantr 276 |
. . . . . . . . . . . 12
⢠((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā š“ ā {š“}) |
37 | | simprl 529 |
. . . . . . . . . . . 12
⢠((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā š¦ ā šµ) |
38 | | opelxpi 4660 |
. . . . . . . . . . . 12
⢠((š“ ā {š“} ā§ š¦ ā šµ) ā āØš“, š¦ā© ā ({š“} Ć šµ)) |
39 | 36, 37, 38 | syl2anc 411 |
. . . . . . . . . . 11
⢠((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā āØš“, š¦ā© ā ({š“} Ć šµ)) |
40 | 34, 39 | eqeltrd 2254 |
. . . . . . . . . 10
⢠((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā š„ ā ({š“} Ć šµ)) |
41 | 33, 40 | jca 306 |
. . . . . . . . 9
⢠((š“ ā š ā§ (š¦ ā šµ ā§ š„ = āØš“, š¦ā©)) ā ((2nd āš„) = š¦ ā§ š„ ā ({š“} Ć šµ))) |
42 | 28, 41 | impbida 596 |
. . . . . . . 8
⢠(š“ ā š ā (((2nd āš„) = š¦ ā§ š„ ā ({š“} Ć šµ)) ā (š¦ ā šµ ā§ š„ = āØš“, š¦ā©))) |
43 | 14, 42 | bitr3id 194 |
. . . . . . 7
⢠(š“ ā š ā ((š„2nd š¦ ā§ š„ ā ({š“} Ć šµ)) ā (š¦ ā šµ ā§ š„ = āØš“, š¦ā©))) |
44 | 7, 43 | bitrid 192 |
. . . . . 6
⢠(š“ ā š ā (š„(2nd ā¾ ({š“} Ć šµ))š¦ ā (š¦ ā šµ ā§ š„ = āØš“, š¦ā©))) |
45 | 44 | mobidv 2062 |
. . . . 5
⢠(š“ ā š ā (ā*š„ š„(2nd ā¾ ({š“} Ć šµ))š¦ ā ā*š„(š¦ ā šµ ā§ š„ = āØš“, š¦ā©))) |
46 | 5, 45 | mpbiri 168 |
. . . 4
⢠(š“ ā š ā ā*š„ š„(2nd ā¾ ({š“} Ć šµ))š¦) |
47 | 46 | alrimiv 1874 |
. . 3
⢠(š“ ā š ā āš¦ā*š„ š„(2nd ā¾ ({š“} Ć šµ))š¦) |
48 | | funcnv2 5278 |
. . 3
⢠(Fun
ā”(2nd ā¾ ({š“} Ć šµ)) ā āš¦ā*š„ š„(2nd ā¾ ({š“} Ć šµ))š¦) |
49 | 47, 48 | sylibr 134 |
. 2
⢠(š“ ā š ā Fun ā”(2nd ā¾ ({š“} Ć šµ))) |
50 | | dff1o3 5469 |
. 2
ā¢
((2nd ā¾ ({š“} Ć šµ)):({š“} Ć šµ)ā1-1-ontoāšµ ā ((2nd ā¾
({š“} Ć šµ)):({š“} Ć šµ)āontoāšµ ā§ Fun ā”(2nd ā¾ ({š“} Ć šµ)))) |
51 | 3, 49, 50 | sylanbrc 417 |
1
⢠(š“ ā š ā (2nd ā¾ ({š“} Ć šµ)):({š“} Ć šµ)ā1-1-ontoāšµ) |