Step | Hyp | Ref
| Expression |
1 | | mptexg 5741 |
. . . 4
ā¢ (š“ ā š· ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) ā V) |
2 | | eueq 2908 |
. . . 4
ā¢ ((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) ā V ā ā!ā ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) |
3 | 1, 2 | sylib 122 |
. . 3
ā¢ (š“ ā š· ā ā!ā ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) |
4 | 3 | 3ad2ant1 1018 |
. 2
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā ā!ā ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) |
5 | | ffn 5365 |
. . . . . . . 8
ā¢ (ā:š“ā¶(šµ Ć š¶) ā ā Fn š“) |
6 | 5 | 3ad2ant1 1018 |
. . . . . . 7
ā¢ ((ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā)) ā ā Fn š“) |
7 | 6 | adantl 277 |
. . . . . 6
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā ā Fn š“) |
8 | | ffvelcdm 5649 |
. . . . . . . . . . . . 13
ā¢ ((š¹:š“ā¶šµ ā§ š„ ā š“) ā (š¹āš„) ā šµ) |
9 | | ffvelcdm 5649 |
. . . . . . . . . . . . 13
ā¢ ((šŗ:š“ā¶š¶ ā§ š„ ā š“) ā (šŗāš„) ā š¶) |
10 | | opelxpi 4658 |
. . . . . . . . . . . . 13
ā¢ (((š¹āš„) ā šµ ā§ (šŗāš„) ā š¶) ā āØ(š¹āš„), (šŗāš„)ā© ā (šµ Ć š¶)) |
11 | 8, 9, 10 | syl2an 289 |
. . . . . . . . . . . 12
ā¢ (((š¹:š“ā¶šµ ā§ š„ ā š“) ā§ (šŗ:š“ā¶š¶ ā§ š„ ā š“)) ā āØ(š¹āš„), (šŗāš„)ā© ā (šµ Ć š¶)) |
12 | 11 | anandirs 593 |
. . . . . . . . . . 11
ā¢ (((š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š„ ā š“) ā āØ(š¹āš„), (šŗāš„)ā© ā (šµ Ć š¶)) |
13 | 12 | ralrimiva 2550 |
. . . . . . . . . 10
ā¢ ((š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā āš„ ā š“ āØ(š¹āš„), (šŗāš„)ā© ā (šµ Ć š¶)) |
14 | 13 | 3adant1 1015 |
. . . . . . . . 9
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā āš„ ā š“ āØ(š¹āš„), (šŗāš„)ā© ā (šµ Ć š¶)) |
15 | | eqid 2177 |
. . . . . . . . . 10
ā¢ (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) |
16 | 15 | fmpt 5666 |
. . . . . . . . 9
ā¢
(āš„ ā
š“ āØ(š¹āš„), (šŗāš„)ā© ā (šµ Ć š¶) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©):š“ā¶(šµ Ć š¶)) |
17 | 14, 16 | sylib 122 |
. . . . . . . 8
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©):š“ā¶(šµ Ć š¶)) |
18 | 17 | ffnd 5366 |
. . . . . . 7
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) Fn š“) |
19 | 18 | adantr 276 |
. . . . . 6
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) Fn š“) |
20 | | xpss 4734 |
. . . . . . . . . . 11
ā¢ (šµ Ć š¶) ā (V Ć V) |
21 | | ffvelcdm 5649 |
. . . . . . . . . . 11
ā¢ ((ā:š“ā¶(šµ Ć š¶) ā§ š§ ā š“) ā (āāš§) ā (šµ Ć š¶)) |
22 | 20, 21 | sselid 3153 |
. . . . . . . . . 10
ā¢ ((ā:š“ā¶(šµ Ć š¶) ā§ š§ ā š“) ā (āāš§) ā (V Ć V)) |
23 | 22 | 3ad2antl1 1159 |
. . . . . . . . 9
ā¢ (((ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā)) ā§ š§ ā š“) ā (āāš§) ā (V Ć V)) |
24 | 23 | adantll 476 |
. . . . . . . 8
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā (āāš§) ā (V Ć V)) |
25 | | fveq1 5514 |
. . . . . . . . . . . 12
ā¢ (š¹ = (š ā ā) ā (š¹āš§) = ((š ā ā)āš§)) |
26 | | upxp.1 |
. . . . . . . . . . . . . 14
ā¢ š = (1st ā¾
(šµ Ć š¶)) |
27 | 26 | coeq1i 4786 |
. . . . . . . . . . . . 13
ā¢ (š ā ā) = ((1st ā¾ (šµ Ć š¶)) ā ā) |
28 | 27 | fveq1i 5516 |
. . . . . . . . . . . 12
ā¢ ((š ā ā)āš§) = (((1st ā¾ (šµ Ć š¶)) ā ā)āš§) |
29 | 25, 28 | eqtrdi 2226 |
. . . . . . . . . . 11
ā¢ (š¹ = (š ā ā) ā (š¹āš§) = (((1st ā¾ (šµ Ć š¶)) ā ā)āš§)) |
30 | 29 | 3ad2ant2 1019 |
. . . . . . . . . 10
ā¢ ((ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā)) ā (š¹āš§) = (((1st ā¾ (šµ Ć š¶)) ā ā)āš§)) |
31 | 30 | ad2antlr 489 |
. . . . . . . . 9
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā (š¹āš§) = (((1st ā¾ (šµ Ć š¶)) ā ā)āš§)) |
32 | | simpr1 1003 |
. . . . . . . . . 10
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā ā:š“ā¶(šµ Ć š¶)) |
33 | | fvco3 5587 |
. . . . . . . . . 10
ā¢ ((ā:š“ā¶(šµ Ć š¶) ā§ š§ ā š“) ā (((1st ā¾ (šµ Ć š¶)) ā ā)āš§) = ((1st ā¾ (šµ Ć š¶))ā(āāš§))) |
34 | 32, 33 | sylan 283 |
. . . . . . . . 9
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā (((1st ā¾ (šµ Ć š¶)) ā ā)āš§) = ((1st ā¾ (šµ Ć š¶))ā(āāš§))) |
35 | 21 | 3ad2antl1 1159 |
. . . . . . . . . . 11
ā¢ (((ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā)) ā§ š§ ā š“) ā (āāš§) ā (šµ Ć š¶)) |
36 | 35 | adantll 476 |
. . . . . . . . . 10
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā (āāš§) ā (šµ Ć š¶)) |
37 | 36 | fvresd 5540 |
. . . . . . . . 9
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā ((1st ā¾ (šµ Ć š¶))ā(āāš§)) = (1st ā(āāš§))) |
38 | 31, 34, 37 | 3eqtrrd 2215 |
. . . . . . . 8
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā (1st ā(āāš§)) = (š¹āš§)) |
39 | | fveq1 5514 |
. . . . . . . . . . . 12
ā¢ (šŗ = (š ā ā) ā (šŗāš§) = ((š ā ā)āš§)) |
40 | | upxp.2 |
. . . . . . . . . . . . . 14
ā¢ š = (2nd ā¾
(šµ Ć š¶)) |
41 | 40 | coeq1i 4786 |
. . . . . . . . . . . . 13
ā¢ (š ā ā) = ((2nd ā¾ (šµ Ć š¶)) ā ā) |
42 | 41 | fveq1i 5516 |
. . . . . . . . . . . 12
ā¢ ((š ā ā)āš§) = (((2nd ā¾ (šµ Ć š¶)) ā ā)āš§) |
43 | 39, 42 | eqtrdi 2226 |
. . . . . . . . . . 11
ā¢ (šŗ = (š ā ā) ā (šŗāš§) = (((2nd ā¾ (šµ Ć š¶)) ā ā)āš§)) |
44 | 43 | 3ad2ant3 1020 |
. . . . . . . . . 10
ā¢ ((ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā)) ā (šŗāš§) = (((2nd ā¾ (šµ Ć š¶)) ā ā)āš§)) |
45 | 44 | ad2antlr 489 |
. . . . . . . . 9
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā (šŗāš§) = (((2nd ā¾ (šµ Ć š¶)) ā ā)āš§)) |
46 | | fvco3 5587 |
. . . . . . . . . 10
ā¢ ((ā:š“ā¶(šµ Ć š¶) ā§ š§ ā š“) ā (((2nd ā¾ (šµ Ć š¶)) ā ā)āš§) = ((2nd ā¾ (šµ Ć š¶))ā(āāš§))) |
47 | 32, 46 | sylan 283 |
. . . . . . . . 9
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā (((2nd ā¾ (šµ Ć š¶)) ā ā)āš§) = ((2nd ā¾ (šµ Ć š¶))ā(āāš§))) |
48 | 36 | fvresd 5540 |
. . . . . . . . 9
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā ((2nd ā¾ (šµ Ć š¶))ā(āāš§)) = (2nd ā(āāš§))) |
49 | 45, 47, 48 | 3eqtrrd 2215 |
. . . . . . . 8
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā (2nd ā(āāš§)) = (šŗāš§)) |
50 | | eqopi 6172 |
. . . . . . . 8
ā¢ (((āāš§) ā (V Ć V) ā§ ((1st
ā(āāš§)) = (š¹āš§) ā§ (2nd ā(āāš§)) = (šŗāš§))) ā (āāš§) = āØ(š¹āš§), (šŗāš§)ā©) |
51 | 24, 38, 49, 50 | syl12anc 1236 |
. . . . . . 7
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā (āāš§) = āØ(š¹āš§), (šŗāš§)ā©) |
52 | | fveq2 5515 |
. . . . . . . . 9
ā¢ (š„ = š§ ā (š¹āš„) = (š¹āš§)) |
53 | | fveq2 5515 |
. . . . . . . . 9
ā¢ (š„ = š§ ā (šŗāš„) = (šŗāš§)) |
54 | 52, 53 | opeq12d 3786 |
. . . . . . . 8
ā¢ (š„ = š§ ā āØ(š¹āš„), (šŗāš„)ā© = āØ(š¹āš§), (šŗāš§)ā©) |
55 | | simpr 110 |
. . . . . . . 8
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā š§ ā š“) |
56 | 51, 36 | eqeltrrd 2255 |
. . . . . . . 8
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā āØ(š¹āš§), (šŗāš§)ā© ā (šµ Ć š¶)) |
57 | 15, 54, 55, 56 | fvmptd3 5609 |
. . . . . . 7
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā ((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)āš§) = āØ(š¹āš§), (šŗāš§)ā©) |
58 | 51, 57 | eqtr4d 2213 |
. . . . . 6
ā¢ ((((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā§ š§ ā š“) ā (āāš§) = ((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)āš§)) |
59 | 7, 19, 58 | eqfnfvd 5616 |
. . . . 5
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) ā ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) |
60 | 59 | ex 115 |
. . . 4
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā ((ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā)) ā ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))) |
61 | | ffn 5365 |
. . . . . . . . 9
ā¢ (š¹:š“ā¶šµ ā š¹ Fn š“) |
62 | 61 | 3ad2ant2 1019 |
. . . . . . . 8
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā š¹ Fn š“) |
63 | | fo1st 6157 |
. . . . . . . . . . 11
ā¢
1st :VāontoāV |
64 | | fofn 5440 |
. . . . . . . . . . 11
ā¢
(1st :VāontoāV ā 1st Fn V) |
65 | 63, 64 | ax-mp 5 |
. . . . . . . . . 10
ā¢
1st Fn V |
66 | | ssv 3177 |
. . . . . . . . . 10
ā¢ (šµ Ć š¶) ā V |
67 | | fnssres 5329 |
. . . . . . . . . 10
ā¢
((1st Fn V ā§ (šµ Ć š¶) ā V) ā (1st ā¾
(šµ Ć š¶)) Fn (šµ Ć š¶)) |
68 | 65, 66, 67 | mp2an 426 |
. . . . . . . . 9
ā¢
(1st ā¾ (šµ Ć š¶)) Fn (šµ Ć š¶) |
69 | 17 | frnd 5375 |
. . . . . . . . 9
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā ran (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) ā (šµ Ć š¶)) |
70 | | fnco 5324 |
. . . . . . . . 9
ā¢
(((1st ā¾ (šµ Ć š¶)) Fn (šµ Ć š¶) ā§ (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) Fn š“ ā§ ran (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) ā (šµ Ć š¶)) ā ((1st ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) Fn š“) |
71 | 68, 18, 69, 70 | mp3an2i 1342 |
. . . . . . . 8
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā ((1st ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) Fn š“) |
72 | | fvco3 5587 |
. . . . . . . . . 10
ā¢ (((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©):š“ā¶(šµ Ć š¶) ā§ š§ ā š“) ā (((1st ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))āš§) = ((1st ā¾ (šµ Ć š¶))ā((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)āš§))) |
73 | 17, 72 | sylan 283 |
. . . . . . . . 9
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā (((1st ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))āš§) = ((1st ā¾ (šµ Ć š¶))ā((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)āš§))) |
74 | | simpr 110 |
. . . . . . . . . . 11
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā š§ ā š“) |
75 | | simpl2 1001 |
. . . . . . . . . . . . 13
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā š¹:š“ā¶šµ) |
76 | 75, 74 | ffvelcdmd 5652 |
. . . . . . . . . . . 12
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā (š¹āš§) ā šµ) |
77 | | simpl3 1002 |
. . . . . . . . . . . . 13
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā šŗ:š“ā¶š¶) |
78 | 77, 74 | ffvelcdmd 5652 |
. . . . . . . . . . . 12
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā (šŗāš§) ā š¶) |
79 | 76, 78 | opelxpd 4659 |
. . . . . . . . . . 11
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā āØ(š¹āš§), (šŗāš§)ā© ā (šµ Ć š¶)) |
80 | 15, 54, 74, 79 | fvmptd3 5609 |
. . . . . . . . . 10
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā ((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)āš§) = āØ(š¹āš§), (šŗāš§)ā©) |
81 | 80 | fveq2d 5519 |
. . . . . . . . 9
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā ((1st ā¾ (šµ Ć š¶))ā((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)āš§)) = ((1st ā¾ (šµ Ć š¶))āāØ(š¹āš§), (šŗāš§)ā©)) |
82 | | ffvelcdm 5649 |
. . . . . . . . . . . . . 14
ā¢ ((š¹:š“ā¶šµ ā§ š§ ā š“) ā (š¹āš§) ā šµ) |
83 | | ffvelcdm 5649 |
. . . . . . . . . . . . . 14
ā¢ ((šŗ:š“ā¶š¶ ā§ š§ ā š“) ā (šŗāš§) ā š¶) |
84 | | opelxpi 4658 |
. . . . . . . . . . . . . 14
ā¢ (((š¹āš§) ā šµ ā§ (šŗāš§) ā š¶) ā āØ(š¹āš§), (šŗāš§)ā© ā (šµ Ć š¶)) |
85 | 82, 83, 84 | syl2an 289 |
. . . . . . . . . . . . 13
ā¢ (((š¹:š“ā¶šµ ā§ š§ ā š“) ā§ (šŗ:š“ā¶š¶ ā§ š§ ā š“)) ā āØ(š¹āš§), (šŗāš§)ā© ā (šµ Ć š¶)) |
86 | 85 | anandirs 593 |
. . . . . . . . . . . 12
ā¢ (((š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā āØ(š¹āš§), (šŗāš§)ā© ā (šµ Ć š¶)) |
87 | 86 | 3adantl1 1153 |
. . . . . . . . . . 11
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā āØ(š¹āš§), (šŗāš§)ā© ā (šµ Ć š¶)) |
88 | 87 | fvresd 5540 |
. . . . . . . . . 10
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā ((1st ā¾ (šµ Ć š¶))āāØ(š¹āš§), (šŗāš§)ā©) = (1st
āāØ(š¹āš§), (šŗāš§)ā©)) |
89 | | op1stg 6150 |
. . . . . . . . . . 11
ā¢ (((š¹āš§) ā šµ ā§ (šŗāš§) ā š¶) ā (1st āāØ(š¹āš§), (šŗāš§)ā©) = (š¹āš§)) |
90 | 76, 78, 89 | syl2anc 411 |
. . . . . . . . . 10
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā (1st āāØ(š¹āš§), (šŗāš§)ā©) = (š¹āš§)) |
91 | 88, 90 | eqtrd 2210 |
. . . . . . . . 9
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā ((1st ā¾ (šµ Ć š¶))āāØ(š¹āš§), (šŗāš§)ā©) = (š¹āš§)) |
92 | 73, 81, 91 | 3eqtrrd 2215 |
. . . . . . . 8
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā (š¹āš§) = (((1st ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))āš§)) |
93 | 62, 71, 92 | eqfnfvd 5616 |
. . . . . . 7
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā š¹ = ((1st ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))) |
94 | 26 | coeq1i 4786 |
. . . . . . 7
ā¢ (š ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) = ((1st ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) |
95 | 93, 94 | eqtr4di 2228 |
. . . . . 6
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā š¹ = (š ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))) |
96 | | ffn 5365 |
. . . . . . . . 9
ā¢ (šŗ:š“ā¶š¶ ā šŗ Fn š“) |
97 | 96 | 3ad2ant3 1020 |
. . . . . . . 8
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā šŗ Fn š“) |
98 | | fo2nd 6158 |
. . . . . . . . . . 11
ā¢
2nd :VāontoāV |
99 | | fofn 5440 |
. . . . . . . . . . 11
ā¢
(2nd :VāontoāV ā 2nd Fn V) |
100 | 98, 99 | ax-mp 5 |
. . . . . . . . . 10
ā¢
2nd Fn V |
101 | | fnssres 5329 |
. . . . . . . . . 10
ā¢
((2nd Fn V ā§ (šµ Ć š¶) ā V) ā (2nd ā¾
(šµ Ć š¶)) Fn (šµ Ć š¶)) |
102 | 100, 66, 101 | mp2an 426 |
. . . . . . . . 9
ā¢
(2nd ā¾ (šµ Ć š¶)) Fn (šµ Ć š¶) |
103 | | fnco 5324 |
. . . . . . . . 9
ā¢
(((2nd ā¾ (šµ Ć š¶)) Fn (šµ Ć š¶) ā§ (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) Fn š“ ā§ ran (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) ā (šµ Ć š¶)) ā ((2nd ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) Fn š“) |
104 | 102, 18, 69, 103 | mp3an2i 1342 |
. . . . . . . 8
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā ((2nd ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) Fn š“) |
105 | | fvco3 5587 |
. . . . . . . . . 10
ā¢ (((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©):š“ā¶(šµ Ć š¶) ā§ š§ ā š“) ā (((2nd ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))āš§) = ((2nd ā¾ (šµ Ć š¶))ā((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)āš§))) |
106 | 17, 105 | sylan 283 |
. . . . . . . . 9
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā (((2nd ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))āš§) = ((2nd ā¾ (šµ Ć š¶))ā((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)āš§))) |
107 | 80 | fveq2d 5519 |
. . . . . . . . 9
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā ((2nd ā¾ (šµ Ć š¶))ā((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)āš§)) = ((2nd ā¾ (šµ Ć š¶))āāØ(š¹āš§), (šŗāš§)ā©)) |
108 | 87 | fvresd 5540 |
. . . . . . . . . 10
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā ((2nd ā¾ (šµ Ć š¶))āāØ(š¹āš§), (šŗāš§)ā©) = (2nd
āāØ(š¹āš§), (šŗāš§)ā©)) |
109 | | op2ndg 6151 |
. . . . . . . . . . 11
ā¢ (((š¹āš§) ā šµ ā§ (šŗāš§) ā š¶) ā (2nd āāØ(š¹āš§), (šŗāš§)ā©) = (šŗāš§)) |
110 | 76, 78, 109 | syl2anc 411 |
. . . . . . . . . 10
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā (2nd āāØ(š¹āš§), (šŗāš§)ā©) = (šŗāš§)) |
111 | 108, 110 | eqtrd 2210 |
. . . . . . . . 9
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā ((2nd ā¾ (šµ Ć š¶))āāØ(š¹āš§), (šŗāš§)ā©) = (šŗāš§)) |
112 | 106, 107,
111 | 3eqtrrd 2215 |
. . . . . . . 8
ā¢ (((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā§ š§ ā š“) ā (šŗāš§) = (((2nd ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))āš§)) |
113 | 97, 104, 112 | eqfnfvd 5616 |
. . . . . . 7
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā šŗ = ((2nd ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))) |
114 | 40 | coeq1i 4786 |
. . . . . . 7
ā¢ (š ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) = ((2nd ā¾ (šµ Ć š¶)) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) |
115 | 113, 114 | eqtr4di 2228 |
. . . . . 6
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā šŗ = (š ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))) |
116 | 17, 95, 115 | 3jca 1177 |
. . . . 5
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā ((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©):š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) ā§ šŗ = (š ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)))) |
117 | | feq1 5348 |
. . . . . 6
ā¢ (ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) ā (ā:š“ā¶(šµ Ć š¶) ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©):š“ā¶(šµ Ć š¶))) |
118 | | coeq2 4785 |
. . . . . . 7
ā¢ (ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) ā (š ā ā) = (š ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))) |
119 | 118 | eqeq2d 2189 |
. . . . . 6
ā¢ (ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) ā (š¹ = (š ā ā) ā š¹ = (š ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)))) |
120 | | coeq2 4785 |
. . . . . . 7
ā¢ (ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) ā (š ā ā) = (š ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))) |
121 | 120 | eqeq2d 2189 |
. . . . . 6
ā¢ (ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) ā (šŗ = (š ā ā) ā šŗ = (š ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)))) |
122 | 117, 119,
121 | 3anbi123d 1312 |
. . . . 5
ā¢ (ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) ā ((ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā)) ā ((š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©):š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©)) ā§ šŗ = (š ā (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))))) |
123 | 116, 122 | syl5ibrcom 157 |
. . . 4
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā (ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©) ā (ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā)))) |
124 | 60, 123 | impbid 129 |
. . 3
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā ((ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā)) ā ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))) |
125 | 124 | eubidv 2034 |
. 2
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā (ā!ā(ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā)) ā ā!ā ā = (š„ ā š“ ā¦ āØ(š¹āš„), (šŗāš„)ā©))) |
126 | 4, 125 | mpbird 167 |
1
ā¢ ((š“ ā š· ā§ š¹:š“ā¶šµ ā§ šŗ:š“ā¶š¶) ā ā!ā(ā:š“ā¶(šµ Ć š¶) ā§ š¹ = (š ā ā) ā§ šŗ = (š ā ā))) |