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