Step | Hyp | Ref
| Expression |
1 | | spanun.1 |
. . . . . . 7
β’ π΄ β
β |
2 | | spancl 30320 |
. . . . . . 7
β’ (π΄ β β β
(spanβπ΄) β
Sβ ) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
β’
(spanβπ΄)
β Sβ |
4 | | spanun.2 |
. . . . . . 7
β’ π΅ β
β |
5 | | spancl 30320 |
. . . . . . 7
β’ (π΅ β β β
(spanβπ΅) β
Sβ ) |
6 | 4, 5 | ax-mp 5 |
. . . . . 6
β’
(spanβπ΅)
β Sβ |
7 | 3, 6 | shscli 30301 |
. . . . 5
β’
((spanβπ΄)
+β (spanβπ΅)) β
Sβ |
8 | 7 | shssii 30197 |
. . . 4
β’
((spanβπ΄)
+β (spanβπ΅)) β β |
9 | | spanss2 30329 |
. . . . . . 7
β’ (π΄ β β β π΄ β (spanβπ΄)) |
10 | 1, 9 | ax-mp 5 |
. . . . . 6
β’ π΄ β (spanβπ΄) |
11 | | spanss2 30329 |
. . . . . . 7
β’ (π΅ β β β π΅ β (spanβπ΅)) |
12 | 4, 11 | ax-mp 5 |
. . . . . 6
β’ π΅ β (spanβπ΅) |
13 | | unss12 4147 |
. . . . . 6
β’ ((π΄ β (spanβπ΄) β§ π΅ β (spanβπ΅)) β (π΄ βͺ π΅) β ((spanβπ΄) βͺ (spanβπ΅))) |
14 | 10, 12, 13 | mp2an 691 |
. . . . 5
β’ (π΄ βͺ π΅) β ((spanβπ΄) βͺ (spanβπ΅)) |
15 | 3, 6 | shunssi 30352 |
. . . . 5
β’
((spanβπ΄)
βͺ (spanβπ΅))
β ((spanβπ΄)
+β (spanβπ΅)) |
16 | 14, 15 | sstri 3958 |
. . . 4
β’ (π΄ βͺ π΅) β ((spanβπ΄) +β (spanβπ΅)) |
17 | | spanss 30332 |
. . . 4
β’
((((spanβπ΄)
+β (spanβπ΅)) β β β§ (π΄ βͺ π΅) β ((spanβπ΄) +β (spanβπ΅))) β (spanβ(π΄ βͺ π΅)) β (spanβ((spanβπ΄) +β
(spanβπ΅)))) |
18 | 8, 16, 17 | mp2an 691 |
. . 3
β’
(spanβ(π΄ βͺ
π΅)) β
(spanβ((spanβπ΄)
+β (spanβπ΅))) |
19 | | spanid 30331 |
. . . 4
β’
(((spanβπ΄)
+β (spanβπ΅)) β Sβ
β (spanβ((spanβπ΄) +β (spanβπ΅))) = ((spanβπ΄) +β
(spanβπ΅))) |
20 | 7, 19 | ax-mp 5 |
. . 3
β’
(spanβ((spanβπ΄) +β (spanβπ΅))) = ((spanβπ΄) +β
(spanβπ΅)) |
21 | 18, 20 | sseqtri 3985 |
. 2
β’
(spanβ(π΄ βͺ
π΅)) β
((spanβπ΄)
+β (spanβπ΅)) |
22 | 3, 6 | shseli 30300 |
. . . . 5
β’ (π₯ β ((spanβπ΄) +β
(spanβπ΅)) β
βπ§ β
(spanβπ΄)βπ€ β (spanβπ΅)π₯ = (π§ +β π€)) |
23 | | r2ex 3193 |
. . . . 5
β’
(βπ§ β
(spanβπ΄)βπ€ β (spanβπ΅)π₯ = (π§ +β π€) β βπ§βπ€((π§ β (spanβπ΄) β§ π€ β (spanβπ΅)) β§ π₯ = (π§ +β π€))) |
24 | 22, 23 | bitri 275 |
. . . 4
β’ (π₯ β ((spanβπ΄) +β
(spanβπ΅)) β
βπ§βπ€((π§ β (spanβπ΄) β§ π€ β (spanβπ΅)) β§ π₯ = (π§ +β π€))) |
25 | | vex 3452 |
. . . . . . . . . . 11
β’ π§ β V |
26 | 25 | elspani 30527 |
. . . . . . . . . 10
β’ (π΄ β β β (π§ β (spanβπ΄) β βπ¦ β
Sβ (π΄ β π¦ β π§ β π¦))) |
27 | 1, 26 | ax-mp 5 |
. . . . . . . . 9
β’ (π§ β (spanβπ΄) β βπ¦ β
Sβ (π΄ β π¦ β π§ β π¦)) |
28 | | vex 3452 |
. . . . . . . . . . 11
β’ π€ β V |
29 | 28 | elspani 30527 |
. . . . . . . . . 10
β’ (π΅ β β β (π€ β (spanβπ΅) β βπ¦ β
Sβ (π΅ β π¦ β π€ β π¦))) |
30 | 4, 29 | ax-mp 5 |
. . . . . . . . 9
β’ (π€ β (spanβπ΅) β βπ¦ β
Sβ (π΅ β π¦ β π€ β π¦)) |
31 | 27, 30 | anbi12i 628 |
. . . . . . . 8
β’ ((π§ β (spanβπ΄) β§ π€ β (spanβπ΅)) β (βπ¦ β Sβ
(π΄ β π¦ β π§ β π¦) β§ βπ¦ β Sβ
(π΅ β π¦ β π€ β π¦))) |
32 | | r19.26 3115 |
. . . . . . . 8
β’
(βπ¦ β
Sβ ((π΄ β π¦ β π§ β π¦) β§ (π΅ β π¦ β π€ β π¦)) β (βπ¦ β Sβ
(π΄ β π¦ β π§ β π¦) β§ βπ¦ β Sβ
(π΅ β π¦ β π€ β π¦))) |
33 | 31, 32 | bitr4i 278 |
. . . . . . 7
β’ ((π§ β (spanβπ΄) β§ π€ β (spanβπ΅)) β βπ¦ β Sβ
((π΄ β π¦ β π§ β π¦) β§ (π΅ β π¦ β π€ β π¦))) |
34 | | r19.27v 3185 |
. . . . . . 7
β’
((βπ¦ β
Sβ ((π΄ β π¦ β π§ β π¦) β§ (π΅ β π¦ β π€ β π¦)) β§ π₯ = (π§ +β π€)) β βπ¦ β Sβ
(((π΄ β π¦ β π§ β π¦) β§ (π΅ β π¦ β π€ β π¦)) β§ π₯ = (π§ +β π€))) |
35 | 33, 34 | sylanb 582 |
. . . . . 6
β’ (((π§ β (spanβπ΄) β§ π€ β (spanβπ΅)) β§ π₯ = (π§ +β π€)) β βπ¦ β Sβ
(((π΄ β π¦ β π§ β π¦) β§ (π΅ β π¦ β π€ β π¦)) β§ π₯ = (π§ +β π€))) |
36 | | unss 4149 |
. . . . . . . . . . . 12
β’ ((π΄ β π¦ β§ π΅ β π¦) β (π΄ βͺ π΅) β π¦) |
37 | | anim12 808 |
. . . . . . . . . . . 12
β’ (((π΄ β π¦ β π§ β π¦) β§ (π΅ β π¦ β π€ β π¦)) β ((π΄ β π¦ β§ π΅ β π¦) β (π§ β π¦ β§ π€ β π¦))) |
38 | 36, 37 | biimtrrid 242 |
. . . . . . . . . . 11
β’ (((π΄ β π¦ β π§ β π¦) β§ (π΅ β π¦ β π€ β π¦)) β ((π΄ βͺ π΅) β π¦ β (π§ β π¦ β§ π€ β π¦))) |
39 | | shaddcl 30201 |
. . . . . . . . . . . 12
β’ ((π¦ β
Sβ β§ π§ β π¦ β§ π€ β π¦) β (π§ +β π€) β π¦) |
40 | 39 | 3expib 1123 |
. . . . . . . . . . 11
β’ (π¦ β
Sβ β ((π§ β π¦ β§ π€ β π¦) β (π§ +β π€) β π¦)) |
41 | 38, 40 | sylan9r 510 |
. . . . . . . . . 10
β’ ((π¦ β
Sβ β§ ((π΄ β π¦ β π§ β π¦) β§ (π΅ β π¦ β π€ β π¦))) β ((π΄ βͺ π΅) β π¦ β (π§ +β π€) β π¦)) |
42 | | eleq1 2826 |
. . . . . . . . . . 11
β’ (π₯ = (π§ +β π€) β (π₯ β π¦ β (π§ +β π€) β π¦)) |
43 | 42 | biimprd 248 |
. . . . . . . . . 10
β’ (π₯ = (π§ +β π€) β ((π§ +β π€) β π¦ β π₯ β π¦)) |
44 | 41, 43 | sylan9 509 |
. . . . . . . . 9
β’ (((π¦ β
Sβ β§ ((π΄ β π¦ β π§ β π¦) β§ (π΅ β π¦ β π€ β π¦))) β§ π₯ = (π§ +β π€)) β ((π΄ βͺ π΅) β π¦ β π₯ β π¦)) |
45 | 44 | expl 459 |
. . . . . . . 8
β’ (π¦ β
Sβ β ((((π΄ β π¦ β π§ β π¦) β§ (π΅ β π¦ β π€ β π¦)) β§ π₯ = (π§ +β π€)) β ((π΄ βͺ π΅) β π¦ β π₯ β π¦))) |
46 | 45 | ralimia 3084 |
. . . . . . 7
β’
(βπ¦ β
Sβ (((π΄ β π¦ β π§ β π¦) β§ (π΅ β π¦ β π€ β π¦)) β§ π₯ = (π§ +β π€)) β βπ¦ β Sβ
((π΄ βͺ π΅) β π¦ β π₯ β π¦)) |
47 | 1, 4 | unssi 4150 |
. . . . . . . 8
β’ (π΄ βͺ π΅) β β |
48 | | vex 3452 |
. . . . . . . . 9
β’ π₯ β V |
49 | 48 | elspani 30527 |
. . . . . . . 8
β’ ((π΄ βͺ π΅) β β β (π₯ β (spanβ(π΄ βͺ π΅)) β βπ¦ β Sβ
((π΄ βͺ π΅) β π¦ β π₯ β π¦))) |
50 | 47, 49 | ax-mp 5 |
. . . . . . 7
β’ (π₯ β (spanβ(π΄ βͺ π΅)) β βπ¦ β Sβ
((π΄ βͺ π΅) β π¦ β π₯ β π¦)) |
51 | 46, 50 | sylibr 233 |
. . . . . 6
β’
(βπ¦ β
Sβ (((π΄ β π¦ β π§ β π¦) β§ (π΅ β π¦ β π€ β π¦)) β§ π₯ = (π§ +β π€)) β π₯ β (spanβ(π΄ βͺ π΅))) |
52 | 35, 51 | syl 17 |
. . . . 5
β’ (((π§ β (spanβπ΄) β§ π€ β (spanβπ΅)) β§ π₯ = (π§ +β π€)) β π₯ β (spanβ(π΄ βͺ π΅))) |
53 | 52 | exlimivv 1936 |
. . . 4
β’
(βπ§βπ€((π§ β (spanβπ΄) β§ π€ β (spanβπ΅)) β§ π₯ = (π§ +β π€)) β π₯ β (spanβ(π΄ βͺ π΅))) |
54 | 24, 53 | sylbi 216 |
. . 3
β’ (π₯ β ((spanβπ΄) +β
(spanβπ΅)) β
π₯ β (spanβ(π΄ βͺ π΅))) |
55 | 54 | ssriv 3953 |
. 2
β’
((spanβπ΄)
+β (spanβπ΅)) β (spanβ(π΄ βͺ π΅)) |
56 | 21, 55 | eqssi 3965 |
1
β’
(spanβ(π΄ βͺ
π΅)) = ((spanβπ΄) +β
(spanβπ΅)) |