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