Step | Hyp | Ref
| Expression |
1 | | fo2nd 7943 |
. . . 4
ā¢
2nd :VāontoāV |
2 | | fofn 6759 |
. . . 4
ā¢
(2nd :VāontoāV ā 2nd Fn V) |
3 | 1, 2 | ax-mp 5 |
. . 3
ā¢
2nd Fn V |
4 | | ffn 6669 |
. . . 4
ā¢ (š¹:š“ā¶(šµ Ć š¶) ā š¹ Fn š“) |
5 | | dffn2 6671 |
. . . 4
ā¢ (š¹ Fn š“ ā š¹:š“ā¶V) |
6 | 4, 5 | sylib 217 |
. . 3
ā¢ (š¹:š“ā¶(šµ Ć š¶) ā š¹:š“ā¶V) |
7 | | fnfco 6708 |
. . 3
ā¢
((2nd Fn V ā§ š¹:š“ā¶V) ā (2nd ā
š¹) Fn š“) |
8 | 3, 6, 7 | sylancr 588 |
. 2
ā¢ (š¹:š“ā¶(šµ Ć š¶) ā (2nd ā š¹) Fn š“) |
9 | | rnco 6205 |
. . 3
ā¢ ran
(2nd ā š¹)
= ran (2nd ā¾ ran š¹) |
10 | | frn 6676 |
. . . . 5
ā¢ (š¹:š“ā¶(šµ Ć š¶) ā ran š¹ ā (šµ Ć š¶)) |
11 | | ssres2 5966 |
. . . . 5
ā¢ (ran
š¹ ā (šµ Ć š¶) ā (2nd ā¾ ran š¹) ā (2nd
ā¾ (šµ Ć š¶))) |
12 | | rnss 5895 |
. . . . 5
ā¢
((2nd ā¾ ran š¹) ā (2nd ā¾ (šµ Ć š¶)) ā ran (2nd ā¾ ran
š¹) ā ran
(2nd ā¾ (šµ
Ć š¶))) |
13 | 10, 11, 12 | 3syl 18 |
. . . 4
ā¢ (š¹:š“ā¶(šµ Ć š¶) ā ran (2nd ā¾ ran
š¹) ā ran
(2nd ā¾ (šµ
Ć š¶))) |
14 | | f2ndres 7947 |
. . . . 5
ā¢
(2nd ā¾ (šµ Ć š¶)):(šµ Ć š¶)ā¶š¶ |
15 | | frn 6676 |
. . . . 5
ā¢
((2nd ā¾ (šµ Ć š¶)):(šµ Ć š¶)ā¶š¶ ā ran (2nd ā¾ (šµ Ć š¶)) ā š¶) |
16 | 14, 15 | ax-mp 5 |
. . . 4
ā¢ ran
(2nd ā¾ (šµ
Ć š¶)) ā š¶ |
17 | 13, 16 | sstrdi 3957 |
. . 3
ā¢ (š¹:š“ā¶(šµ Ć š¶) ā ran (2nd ā¾ ran
š¹) ā š¶) |
18 | 9, 17 | eqsstrid 3993 |
. 2
ā¢ (š¹:š“ā¶(šµ Ć š¶) ā ran (2nd ā š¹) ā š¶) |
19 | | df-f 6501 |
. 2
ā¢
((2nd ā š¹):š“ā¶š¶ ā ((2nd ā š¹) Fn š“ ā§ ran (2nd ā š¹) ā š¶)) |
20 | 8, 18, 19 | sylanbrc 584 |
1
ā¢ (š¹:š“ā¶(šµ Ć š¶) ā (2nd ā š¹):š“ā¶š¶) |