Step | Hyp | Ref
| Expression |
1 | | snnzg 4773 |
. . 3
⢠(šµ ā š ā {šµ} ā ā
) |
2 | | fo1stres 8000 |
. . 3
⢠({šµ} ā ā
ā
(1st ā¾ (š“
Ć {šµ})):(š“ Ć {šµ})āontoāš“) |
3 | 1, 2 | syl 17 |
. 2
⢠(šµ ā š ā (1st ā¾ (š“ Ć {šµ})):(š“ Ć {šµ})āontoāš“) |
4 | | moeq 3698 |
. . . . . 6
ā¢
ā*š„ š„ = āØš¦, šµā© |
5 | 4 | moani 2541 |
. . . . 5
ā¢
ā*š„(š¦ ā š“ ā§ š„ = āØš¦, šµā©) |
6 | | vex 3472 |
. . . . . . . 8
⢠š¦ ā V |
7 | 6 | brresi 5984 |
. . . . . . 7
⢠(š„(1st ā¾ (š“ Ć {šµ}))š¦ ā (š„ ā (š“ Ć {šµ}) ā§ š„1st š¦)) |
8 | | fo1st 7994 |
. . . . . . . . . . 11
ā¢
1st :VāontoāV |
9 | | fofn 6801 |
. . . . . . . . . . 11
ā¢
(1st :VāontoāV ā 1st Fn V) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . 10
ā¢
1st Fn V |
11 | | vex 3472 |
. . . . . . . . . 10
⢠š„ ā V |
12 | | fnbrfvb 6938 |
. . . . . . . . . 10
ā¢
((1st Fn V ā§ š„ ā V) ā ((1st
āš„) = š¦ ā š„1st š¦)) |
13 | 10, 11, 12 | mp2an 689 |
. . . . . . . . 9
ā¢
((1st āš„) = š¦ ā š„1st š¦) |
14 | 13 | anbi2i 622 |
. . . . . . . 8
⢠((š„ ā (š“ Ć {šµ}) ā§ (1st āš„) = š¦) ā (š„ ā (š“ Ć {šµ}) ā§ š„1st š¦)) |
15 | | elxp7 8009 |
. . . . . . . . . . 11
⢠(š„ ā (š“ Ć {šµ}) ā (š„ ā (V Ć V) ā§ ((1st
āš„) ā š“ ā§ (2nd
āš„) ā {šµ}))) |
16 | | eleq1 2815 |
. . . . . . . . . . . . . . 15
ā¢
((1st āš„) = š¦ ā ((1st āš„) ā š“ ā š¦ ā š“)) |
17 | 16 | biimpac 478 |
. . . . . . . . . . . . . 14
ā¢
(((1st āš„) ā š“ ā§ (1st āš„) = š¦) ā š¦ ā š“) |
18 | 17 | adantlr 712 |
. . . . . . . . . . . . 13
ā¢
((((1st āš„) ā š“ ā§ (2nd āš„) ā {šµ}) ā§ (1st āš„) = š¦) ā š¦ ā š“) |
19 | 18 | adantll 711 |
. . . . . . . . . . . 12
⢠(((š„ ā (V Ć V) ā§
((1st āš„)
ā š“ ā§
(2nd āš„)
ā {šµ})) ā§
(1st āš„) =
š¦) ā š¦ ā š“) |
20 | | elsni 4640 |
. . . . . . . . . . . . . 14
ā¢
((2nd āš„) ā {šµ} ā (2nd āš„) = šµ) |
21 | | eqopi 8010 |
. . . . . . . . . . . . . . 15
⢠((š„ ā (V Ć V) ā§
((1st āš„)
= š¦ ā§ (2nd
āš„) = šµ)) ā š„ = āØš¦, šµā©) |
22 | 21 | anass1rs 652 |
. . . . . . . . . . . . . 14
⢠(((š„ ā (V Ć V) ā§
(2nd āš„) =
šµ) ā§ (1st
āš„) = š¦) ā š„ = āØš¦, šµā©) |
23 | 20, 22 | sylanl2 678 |
. . . . . . . . . . . . 13
⢠(((š„ ā (V Ć V) ā§
(2nd āš„)
ā {šµ}) ā§
(1st āš„) =
š¦) ā š„ = āØš¦, šµā©) |
24 | 23 | adantlrl 717 |
. . . . . . . . . . . 12
⢠(((š„ ā (V Ć V) ā§
((1st āš„)
ā š“ ā§
(2nd āš„)
ā {šµ})) ā§
(1st āš„) =
š¦) ā š„ = āØš¦, šµā©) |
25 | 19, 24 | jca 511 |
. . . . . . . . . . 11
⢠(((š„ ā (V Ć V) ā§
((1st āš„)
ā š“ ā§
(2nd āš„)
ā {šµ})) ā§
(1st āš„) =
š¦) ā (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) |
26 | 15, 25 | sylanb 580 |
. . . . . . . . . 10
⢠((š„ ā (š“ Ć {šµ}) ā§ (1st āš„) = š¦) ā (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) |
27 | 26 | adantl 481 |
. . . . . . . . 9
⢠((šµ ā š ā§ (š„ ā (š“ Ć {šµ}) ā§ (1st āš„) = š¦)) ā (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) |
28 | | simprr 770 |
. . . . . . . . . . 11
⢠((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā š„ = āØš¦, šµā©) |
29 | | simprl 768 |
. . . . . . . . . . . 12
⢠((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā š¦ ā š“) |
30 | | snidg 4657 |
. . . . . . . . . . . . 13
⢠(šµ ā š ā šµ ā {šµ}) |
31 | 30 | adantr 480 |
. . . . . . . . . . . 12
⢠((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā šµ ā {šµ}) |
32 | 29, 31 | opelxpd 5708 |
. . . . . . . . . . 11
⢠((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā āØš¦, šµā© ā (š“ Ć {šµ})) |
33 | 28, 32 | eqeltrd 2827 |
. . . . . . . . . 10
⢠((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā š„ ā (š“ Ć {šµ})) |
34 | 28 | fveq2d 6889 |
. . . . . . . . . . 11
⢠((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā (1st āš„) = (1st
āāØš¦, šµā©)) |
35 | | simpl 482 |
. . . . . . . . . . . 12
⢠((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā šµ ā š) |
36 | | op1stg 7986 |
. . . . . . . . . . . 12
⢠((š¦ ā š“ ā§ šµ ā š) ā (1st āāØš¦, šµā©) = š¦) |
37 | 29, 35, 36 | syl2anc 583 |
. . . . . . . . . . 11
⢠((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā (1st
āāØš¦, šµā©) = š¦) |
38 | 34, 37 | eqtrd 2766 |
. . . . . . . . . 10
⢠((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā (1st āš„) = š¦) |
39 | 33, 38 | jca 511 |
. . . . . . . . 9
⢠((šµ ā š ā§ (š¦ ā š“ ā§ š„ = āØš¦, šµā©)) ā (š„ ā (š“ Ć {šµ}) ā§ (1st āš„) = š¦)) |
40 | 27, 39 | impbida 798 |
. . . . . . . 8
⢠(šµ ā š ā ((š„ ā (š“ Ć {šµ}) ā§ (1st āš„) = š¦) ā (š¦ ā š“ ā§ š„ = āØš¦, šµā©))) |
41 | 14, 40 | bitr3id 285 |
. . . . . . 7
⢠(šµ ā š ā ((š„ ā (š“ Ć {šµ}) ā§ š„1st š¦) ā (š¦ ā š“ ā§ š„ = āØš¦, šµā©))) |
42 | 7, 41 | bitrid 283 |
. . . . . 6
⢠(šµ ā š ā (š„(1st ā¾ (š“ Ć {šµ}))š¦ ā (š¦ ā š“ ā§ š„ = āØš¦, šµā©))) |
43 | 42 | mobidv 2537 |
. . . . 5
⢠(šµ ā š ā (ā*š„ š„(1st ā¾ (š“ Ć {šµ}))š¦ ā ā*š„(š¦ ā š“ ā§ š„ = āØš¦, šµā©))) |
44 | 5, 43 | mpbiri 258 |
. . . 4
⢠(šµ ā š ā ā*š„ š„(1st ā¾ (š“ Ć {šµ}))š¦) |
45 | 44 | alrimiv 1922 |
. . 3
⢠(šµ ā š ā āš¦ā*š„ š„(1st ā¾ (š“ Ć {šµ}))š¦) |
46 | | funcnv2 6610 |
. . 3
⢠(Fun
ā”(1st ā¾ (š“ Ć {šµ})) ā āš¦ā*š„ š„(1st ā¾ (š“ Ć {šµ}))š¦) |
47 | 45, 46 | sylibr 233 |
. 2
⢠(šµ ā š ā Fun ā”(1st ā¾ (š“ Ć {šµ}))) |
48 | | dff1o3 6833 |
. 2
ā¢
((1st ā¾ (š“ Ć {šµ})):(š“ Ć {šµ})ā1-1-ontoāš“ ā ((1st ā¾
(š“ Ć {šµ})):(š“ Ć {šµ})āontoāš“ ā§ Fun ā”(1st ā¾ (š“ Ć {šµ})))) |
49 | 3, 47, 48 | sylanbrc 582 |
1
⢠(šµ ā š ā (1st ā¾ (š“ Ć {šµ})):(š“ Ć {šµ})ā1-1-ontoāš“) |