Step | Hyp | Ref
| Expression |
1 | | fo2nd 8000 |
. . . 4
ā¢
2nd :VāontoāV |
2 | | fofn 6807 |
. . . 4
ā¢
(2nd :VāontoāV ā 2nd Fn V) |
3 | 1, 2 | ax-mp 5 |
. . 3
ā¢
2nd Fn V |
4 | | ffn 6717 |
. . . 4
⢠(š¹:š“ā¶(šµ Ć š¶) ā š¹ Fn š“) |
5 | | dffn2 6719 |
. . . 4
⢠(š¹ Fn š“ ā š¹:š“ā¶V) |
6 | 4, 5 | sylib 217 |
. . 3
⢠(š¹:š“ā¶(šµ Ć š¶) ā š¹:š“ā¶V) |
7 | | fnfco 6756 |
. . 3
ā¢
((2nd Fn V ā§ š¹:š“ā¶V) ā (2nd ā
š¹) Fn š“) |
8 | 3, 6, 7 | sylancr 586 |
. 2
⢠(š¹:š“ā¶(šµ Ć š¶) ā (2nd ā š¹) Fn š“) |
9 | | rnco 6251 |
. . 3
⢠ran
(2nd ā š¹)
= ran (2nd ā¾ ran š¹) |
10 | | frn 6724 |
. . . . 5
⢠(š¹:š“ā¶(šµ Ć š¶) ā ran š¹ ā (šµ Ć š¶)) |
11 | | ssres2 6009 |
. . . . 5
⢠(ran
š¹ ā (šµ Ć š¶) ā (2nd ā¾ ran š¹) ā (2nd
ā¾ (šµ Ć š¶))) |
12 | | rnss 5938 |
. . . . 5
ā¢
((2nd ā¾ ran š¹) ā (2nd ā¾ (šµ Ć š¶)) ā ran (2nd ā¾ ran
š¹) ā ran
(2nd ā¾ (šµ
Ć š¶))) |
13 | 10, 11, 12 | 3syl 18 |
. . . 4
⢠(š¹:š“ā¶(šµ Ć š¶) ā ran (2nd ā¾ ran
š¹) ā ran
(2nd ā¾ (šµ
Ć š¶))) |
14 | | f2ndres 8004 |
. . . . 5
ā¢
(2nd ā¾ (šµ Ć š¶)):(šµ Ć š¶)ā¶š¶ |
15 | | frn 6724 |
. . . . 5
ā¢
((2nd ā¾ (šµ Ć š¶)):(šµ Ć š¶)ā¶š¶ ā ran (2nd ā¾ (šµ Ć š¶)) ā š¶) |
16 | 14, 15 | ax-mp 5 |
. . . 4
⢠ran
(2nd ā¾ (šµ
Ć š¶)) ā š¶ |
17 | 13, 16 | sstrdi 3994 |
. . 3
⢠(š¹:š“ā¶(šµ Ć š¶) ā ran (2nd ā¾ ran
š¹) ā š¶) |
18 | 9, 17 | eqsstrid 4030 |
. 2
⢠(š¹:š“ā¶(šµ Ć š¶) ā ran (2nd ā š¹) ā š¶) |
19 | | df-f 6547 |
. 2
ā¢
((2nd ā š¹):š“ā¶š¶ ā ((2nd ā š¹) Fn š“ ā§ ran (2nd ā š¹) ā š¶)) |
20 | 8, 18, 19 | sylanbrc 582 |
1
⢠(š¹:š“ā¶(šµ Ć š¶) ā (2nd ā š¹):š“ā¶š¶) |