Step | Hyp | Ref
| Expression |
1 | | snmg 3710 |
. . 3
ā¢ (šµ ā š ā āš„ š„ ā {šµ}) |
2 | | fo1stresm 6161 |
. . 3
ā¢
(āš„ š„ ā {šµ} ā (1st ā¾ (š“ Ć {šµ})):(š“ Ć {šµ})āontoāš“) |
3 | 1, 2 | syl 14 |
. 2
ā¢ (šµ ā š ā (1st ā¾ (š“ Ć {šµ})):(š“ Ć {šµ})āontoāš“) |
4 | | moeq 2912 |
. . . . . 6
ā¢
ā*š„ š„ = āØš¦, šµā© |
5 | 4 | moani 2096 |
. . . . 5
ā¢
ā*š„(š¦ ā š“ ā§ š„ = āØš¦, šµā©) |
6 | | vex 2740 |
. . . . . . . 8
ā¢ š¦ ā V |
7 | 6 | brres 4913 |
. . . . . . 7
ā¢ (š„(1st ā¾ (š“ Ć {šµ}))š¦ ā (š„1st š¦ ā§ š„ ā (š“ Ć {šµ}))) |
8 | | fo1st 6157 |
. . . . . . . . . . 11
ā¢
1st :VāontoāV |
9 | | fofn 5440 |
. . . . . . . . . . 11
ā¢
(1st :VāontoāV ā 1st Fn V) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . 10
ā¢
1st Fn V |
11 | | vex 2740 |
. . . . . . . . . 10
ā¢ š„ ā V |
12 | | fnbrfvb 5556 |
. . . . . . . . . 10
ā¢
((1st Fn V ā§ š„ ā V) ā ((1st
āš„) = š¦ ā š„1st š¦)) |
13 | 10, 11, 12 | mp2an 426 |
. . . . . . . . 9
ā¢
((1st āš„) = š¦ ā š„1st š¦) |
14 | 13 | anbi1i 458 |
. . . . . . . 8
ā¢
(((1st āš„) = š¦ ā§ š„ ā (š“ Ć {šµ})) ā (š„1st š¦ ā§ š„ ā (š“ Ć {šµ}))) |
15 | | elxp7 6170 |
. . . . . . . . . . 11
ā¢ (š„ ā (š“ Ć {šµ}) ā (š„ ā (V Ć V) ā§ ((1st
āš„) ā š“ ā§ (2nd
āš„) ā {šµ}))) |
16 | | eleq1 2240 |
. . . . . . . . . . . . . . 15
ā¢
((1st āš„) = š¦ ā ((1st āš„) ā š“ ā š¦ ā š“)) |
17 | 16 | biimpa 296 |
. . . . . . . . . . . . . 14
ā¢
(((1st āš„) = š¦ ā§ (1st āš„) ā š“) ā š¦ ā š“) |
18 | 17 | adantrr 479 |
. . . . . . . . . . . . 13
ā¢
(((1st āš„) = š¦ ā§ ((1st āš„) ā š“ ā§ (2nd āš„) ā {šµ})) ā š¦ ā š“) |
19 | 18 | adantrl 478 |
. . . . . . . . . . . 12
ā¢
(((1st āš„) = š¦ ā§ (š„ ā (V Ć V) ā§ ((1st
āš„) ā š“ ā§ (2nd
āš„) ā {šµ}))) ā š¦ ā š“) |
20 | | elsni 3610 |
. . . . . . . . . . . . . 14
ā¢
((2nd āš„) ā {šµ} ā (2nd āš„) = šµ) |
21 | | eqopi 6172 |
. . . . . . . . . . . . . . 15
ā¢ ((š„ ā (V Ć V) ā§
((1st āš„)
= š¦ ā§ (2nd
āš„) = šµ)) ā š„ = āØš¦, šµā©) |
22 | 21 | an12s 565 |
. . . . . . . . . . . . . 14
ā¢
(((1st āš„) = š¦ ā§ (š„ ā (V Ć V) ā§ (2nd
āš„) = šµ)) ā š„ = āØš¦, šµā©) |
23 | 20, 22 | sylanr2 405 |
. . . . . . . . . . . . 13
ā¢
(((1st āš„) = š¦ ā§ (š„ ā (V Ć V) ā§ (2nd
āš„) ā {šµ})) ā š„ = āØš¦, šµā©) |
24 | 23 | adantrrl 486 |
. . . . . . . . . . . 12
ā¢
(((1st āš„) = š¦ ā§ (š„ ā (V Ć V) ā§ ((1st
āš„) ā š“ ā§ (2nd
āš„) ā {šµ}))) ā š„ = āØš¦, šµā©) |
25 | 19, 24 | jca 306 |
. . . . . . . . . . 11
ā¢
(((1st āš„) = š¦ ā§ (š„ ā (V Ć V) ā§ ((1st
āš„) ā š“ ā§ (2nd
āš„) ā {šµ}))) ā (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) |
26 | 15, 25 | sylan2b 287 |
. . . . . . . . . 10
ā¢
(((1st āš„) = š¦ ā§ š„ ā (š“ Ć {šµ})) ā (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) |
27 | 26 | adantl 277 |
. . . . . . . . 9
ā¢ ((šµ ā š ā§ ((1st āš„) = š¦ ā§ š„ ā (š“ Ć {šµ}))) ā (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) |
28 | | simprr 531 |
. . . . . . . . . . . 12
ā¢ ((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā š„ = āØš¦, šµā©) |
29 | 28 | fveq2d 5519 |
. . . . . . . . . . 11
ā¢ ((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā (1st āš„) = (1st
āāØš¦, šµā©)) |
30 | | simprl 529 |
. . . . . . . . . . . 12
ā¢ ((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā š¦ ā š“) |
31 | | simpl 109 |
. . . . . . . . . . . 12
ā¢ ((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā šµ ā š) |
32 | | op1stg 6150 |
. . . . . . . . . . . 12
ā¢ ((š¦ ā š“ ā§ šµ ā š) ā (1st āāØš¦, šµā©) = š¦) |
33 | 30, 31, 32 | syl2anc 411 |
. . . . . . . . . . 11
ā¢ ((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā (1st
āāØš¦, šµā©) = š¦) |
34 | 29, 33 | eqtrd 2210 |
. . . . . . . . . 10
ā¢ ((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā (1st āš„) = š¦) |
35 | | snidg 3621 |
. . . . . . . . . . . . 13
ā¢ (šµ ā š ā šµ ā {šµ}) |
36 | 35 | adantr 276 |
. . . . . . . . . . . 12
ā¢ ((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā šµ ā {šµ}) |
37 | | opelxpi 4658 |
. . . . . . . . . . . 12
ā¢ ((š¦ ā š“ ā§ šµ ā {šµ}) ā āØš¦, šµā© ā (š“ Ć {šµ})) |
38 | 30, 36, 37 | syl2anc 411 |
. . . . . . . . . . 11
ā¢ ((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā āØš¦, šµā© ā (š“ Ć {šµ})) |
39 | 28, 38 | eqeltrd 2254 |
. . . . . . . . . 10
ā¢ ((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā š„ ā (š“ Ć {šµ})) |
40 | 34, 39 | jca 306 |
. . . . . . . . 9
ā¢ ((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā ((1st
āš„) = š¦ ā§ š„ ā (š“ Ć {šµ}))) |
41 | 27, 40 | impbida 596 |
. . . . . . . 8
ā¢ (šµ ā š ā (((1st āš„) = š¦ ā§ š„ ā (š“ Ć {šµ})) ā (š¦ ā š“ ā§ š„ = āØš¦, šµā©))) |
42 | 14, 41 | bitr3id 194 |
. . . . . . 7
ā¢ (šµ ā š ā ((š„1st š¦ ā§ š„ ā (š“ Ć {šµ})) ā (š¦ ā š“ ā§ š„ = āØš¦, šµā©))) |
43 | 7, 42 | bitrid 192 |
. . . . . 6
ā¢ (šµ ā š ā (š„(1st ā¾ (š“ Ć {šµ}))š¦ ā (š¦ ā š“ ā§ š„ = āØš¦, šµā©))) |
44 | 43 | mobidv 2062 |
. . . . 5
ā¢ (šµ ā š ā (ā*š„ š„(1st ā¾ (š“ Ć {šµ}))š¦ ā ā*š„(š¦ ā š“ ā§ š„ = āØš¦, šµā©))) |
45 | 5, 44 | mpbiri 168 |
. . . 4
ā¢ (šµ ā š ā ā*š„ š„(1st ā¾ (š“ Ć {šµ}))š¦) |
46 | 45 | alrimiv 1874 |
. . 3
ā¢ (šµ ā š ā āš¦ā*š„ š„(1st ā¾ (š“ Ć {šµ}))š¦) |
47 | | funcnv2 5276 |
. . 3
ā¢ (Fun
ā”(1st ā¾ (š“ Ć {šµ})) ā āš¦ā*š„ š„(1st ā¾ (š“ Ć {šµ}))š¦) |
48 | 46, 47 | sylibr 134 |
. 2
ā¢ (šµ ā š ā Fun ā”(1st ā¾ (š“ Ć {šµ}))) |
49 | | dff1o3 5467 |
. 2
ā¢
((1st ā¾ (š“ Ć {šµ})):(š“ Ć {šµ})ā1-1-ontoāš“ ā ((1st ā¾
(š“ Ć {šµ})):(š“ Ć {šµ})āontoāš“ ā§ Fun ā”(1st ā¾ (š“ Ć {šµ})))) |
50 | 3, 48, 49 | sylanbrc 417 |
1
ā¢ (šµ ā š ā (1st ā¾ (š“ Ć {šµ})):(š“ Ć {šµ})ā1-1-ontoāš“) |