Step | Hyp | Ref
| Expression |
1 | | fo2nd 7946 |
. . . 4
ā¢
2nd :VāontoāV |
2 | | fof 6760 |
. . . 4
ā¢
(2nd :VāontoāV ā 2nd
:Vā¶V) |
3 | | ffn 6672 |
. . . 4
ā¢
(2nd :Vā¶V ā 2nd Fn V) |
4 | 1, 2, 3 | mp2b 10 |
. . 3
ā¢
2nd Fn V |
5 | | ssv 3972 |
. . 3
ā¢ š ā V |
6 | | fnssres 6628 |
. . 3
ā¢
((2nd Fn V ā§ š ā V) ā (2nd ā¾
š) Fn š) |
7 | 4, 5, 6 | mp2an 691 |
. 2
ā¢
(2nd ā¾ š) Fn š |
8 | | df-ima 5650 |
. . 3
ā¢
(2nd ā š) = ran (2nd ā¾ š) |
9 | | iunfo.1 |
. . . . . . . . . . 11
ā¢ š = āŖ š„ ā š“ ({š„} Ć šµ) |
10 | 9 | eleq2i 2826 |
. . . . . . . . . 10
ā¢ (š§ ā š ā š§ ā āŖ
š„ ā š“ ({š„} Ć šµ)) |
11 | | eliun 4962 |
. . . . . . . . . 10
ā¢ (š§ ā āŖ š„ ā š“ ({š„} Ć šµ) ā āš„ ā š“ š§ ā ({š„} Ć šµ)) |
12 | 10, 11 | bitri 275 |
. . . . . . . . 9
ā¢ (š§ ā š ā āš„ ā š“ š§ ā ({š„} Ć šµ)) |
13 | | xp2nd 7958 |
. . . . . . . . . . 11
ā¢ (š§ ā ({š„} Ć šµ) ā (2nd āš§) ā šµ) |
14 | | eleq1 2822 |
. . . . . . . . . . 11
ā¢
((2nd āš§) = š¦ ā ((2nd āš§) ā šµ ā š¦ ā šµ)) |
15 | 13, 14 | imbitrid 243 |
. . . . . . . . . 10
ā¢
((2nd āš§) = š¦ ā (š§ ā ({š„} Ć šµ) ā š¦ ā šµ)) |
16 | 15 | reximdv 3164 |
. . . . . . . . 9
ā¢
((2nd āš§) = š¦ ā (āš„ ā š“ š§ ā ({š„} Ć šµ) ā āš„ ā š“ š¦ ā šµ)) |
17 | 12, 16 | biimtrid 241 |
. . . . . . . 8
ā¢
((2nd āš§) = š¦ ā (š§ ā š ā āš„ ā š“ š¦ ā šµ)) |
18 | 17 | impcom 409 |
. . . . . . 7
ā¢ ((š§ ā š ā§ (2nd āš§) = š¦) ā āš„ ā š“ š¦ ā šµ) |
19 | 18 | rexlimiva 3141 |
. . . . . 6
ā¢
(āš§ ā
š (2nd
āš§) = š¦ ā āš„ ā š“ š¦ ā šµ) |
20 | | nfiu1 4992 |
. . . . . . . . 9
ā¢
ā²š„āŖ š„ ā š“ ({š„} Ć šµ) |
21 | 9, 20 | nfcxfr 2902 |
. . . . . . . 8
ā¢
ā²š„š |
22 | | nfv 1918 |
. . . . . . . 8
ā¢
ā²š„(2nd āš§) = š¦ |
23 | 21, 22 | nfrexw 3295 |
. . . . . . 7
ā¢
ā²š„āš§ ā š (2nd āš§) = š¦ |
24 | | ssiun2 5011 |
. . . . . . . . . . . 12
ā¢ (š„ ā š“ ā ({š„} Ć šµ) ā āŖ š„ ā š“ ({š„} Ć šµ)) |
25 | 24 | adantr 482 |
. . . . . . . . . . 11
ā¢ ((š„ ā š“ ā§ š¦ ā šµ) ā ({š„} Ć šµ) ā āŖ š„ ā š“ ({š„} Ć šµ)) |
26 | | simpr 486 |
. . . . . . . . . . . 12
ā¢ ((š„ ā š“ ā§ š¦ ā šµ) ā š¦ ā šµ) |
27 | | vsnid 4627 |
. . . . . . . . . . . . 13
ā¢ š„ ā {š„} |
28 | | opelxp 5673 |
. . . . . . . . . . . . 13
ā¢
(āØš„, š¦ā© ā ({š„} Ć šµ) ā (š„ ā {š„} ā§ š¦ ā šµ)) |
29 | 27, 28 | mpbiran 708 |
. . . . . . . . . . . 12
ā¢
(āØš„, š¦ā© ā ({š„} Ć šµ) ā š¦ ā šµ) |
30 | 26, 29 | sylibr 233 |
. . . . . . . . . . 11
ā¢ ((š„ ā š“ ā§ š¦ ā šµ) ā āØš„, š¦ā© ā ({š„} Ć šµ)) |
31 | 25, 30 | sseldd 3949 |
. . . . . . . . . 10
ā¢ ((š„ ā š“ ā§ š¦ ā šµ) ā āØš„, š¦ā© ā āŖ š„ ā š“ ({š„} Ć šµ)) |
32 | 31, 9 | eleqtrrdi 2845 |
. . . . . . . . 9
ā¢ ((š„ ā š“ ā§ š¦ ā šµ) ā āØš„, š¦ā© ā š) |
33 | | vex 3451 |
. . . . . . . . . 10
ā¢ š„ ā V |
34 | | vex 3451 |
. . . . . . . . . 10
ā¢ š¦ ā V |
35 | 33, 34 | op2nd 7934 |
. . . . . . . . 9
ā¢
(2nd āāØš„, š¦ā©) = š¦ |
36 | | fveqeq2 6855 |
. . . . . . . . . 10
ā¢ (š§ = āØš„, š¦ā© ā ((2nd āš§) = š¦ ā (2nd āāØš„, š¦ā©) = š¦)) |
37 | 36 | rspcev 3583 |
. . . . . . . . 9
ā¢
((āØš„, š¦ā© ā š ā§ (2nd āāØš„, š¦ā©) = š¦) ā āš§ ā š (2nd āš§) = š¦) |
38 | 32, 35, 37 | sylancl 587 |
. . . . . . . 8
ā¢ ((š„ ā š“ ā§ š¦ ā šµ) ā āš§ ā š (2nd āš§) = š¦) |
39 | 38 | ex 414 |
. . . . . . 7
ā¢ (š„ ā š“ ā (š¦ ā šµ ā āš§ ā š (2nd āš§) = š¦)) |
40 | 23, 39 | rexlimi 3241 |
. . . . . 6
ā¢
(āš„ ā
š“ š¦ ā šµ ā āš§ ā š (2nd āš§) = š¦) |
41 | 19, 40 | impbii 208 |
. . . . 5
ā¢
(āš§ ā
š (2nd
āš§) = š¦ ā āš„ ā š“ š¦ ā šµ) |
42 | | fvelimab 6918 |
. . . . . 6
ā¢
((2nd Fn V ā§ š ā V) ā (š¦ ā (2nd ā š) ā āš§ ā š (2nd āš§) = š¦)) |
43 | 4, 5, 42 | mp2an 691 |
. . . . 5
ā¢ (š¦ ā (2nd ā
š) ā āš§ ā š (2nd āš§) = š¦) |
44 | | eliun 4962 |
. . . . 5
ā¢ (š¦ ā āŖ š„ ā š“ šµ ā āš„ ā š“ š¦ ā šµ) |
45 | 41, 43, 44 | 3bitr4i 303 |
. . . 4
ā¢ (š¦ ā (2nd ā
š) ā š¦ ā āŖ š„ ā š“ šµ) |
46 | 45 | eqriv 2730 |
. . 3
ā¢
(2nd ā š) = āŖ
š„ ā š“ šµ |
47 | 8, 46 | eqtr3i 2763 |
. 2
ā¢ ran
(2nd ā¾ š)
= āŖ š„ ā š“ šµ |
48 | | df-fo 6506 |
. 2
ā¢
((2nd ā¾ š):šāontoāāŖ š„ ā š“ šµ ā ((2nd ā¾ š) Fn š ā§ ran (2nd ā¾ š) = āŖ š„ ā š“ šµ)) |
49 | 7, 47, 48 | mpbir2an 710 |
1
ā¢
(2nd ā¾ š):šāontoāāŖ š„ ā š“ šµ |