Step | Hyp | Ref
| Expression |
1 | | ressbas.b |
. . . . 5
β’ π΅ = (Baseβπ) |
2 | | simp1 1137 |
. . . . . 6
β’ ((π΅ β π΄ β§ π β V β§ π΄ β π) β π΅ β π΄) |
3 | | sseqin2 4176 |
. . . . . 6
β’ (π΅ β π΄ β (π΄ β© π΅) = π΅) |
4 | 2, 3 | sylib 217 |
. . . . 5
β’ ((π΅ β π΄ β§ π β V β§ π΄ β π) β (π΄ β© π΅) = π΅) |
5 | | ressbas.r |
. . . . . . 7
β’ π
= (π βΎs π΄) |
6 | 5, 1 | ressid2 17121 |
. . . . . 6
β’ ((π΅ β π΄ β§ π β V β§ π΄ β π) β π
= π) |
7 | 6 | fveq2d 6847 |
. . . . 5
β’ ((π΅ β π΄ β§ π β V β§ π΄ β π) β (Baseβπ
) = (Baseβπ)) |
8 | 1, 4, 7 | 3eqtr4a 2799 |
. . . 4
β’ ((π΅ β π΄ β§ π β V β§ π΄ β π) β (π΄ β© π΅) = (Baseβπ
)) |
9 | 8 | 3expib 1123 |
. . 3
β’ (π΅ β π΄ β ((π β V β§ π΄ β π) β (π΄ β© π΅) = (Baseβπ
))) |
10 | | simp2 1138 |
. . . . . 6
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β π) β π β V) |
11 | 1 | fvexi 6857 |
. . . . . . 7
β’ π΅ β V |
12 | 11 | inex2 5276 |
. . . . . 6
β’ (π΄ β© π΅) β V |
13 | | baseid 17091 |
. . . . . . 7
β’ Base =
Slot (Baseβndx) |
14 | 13 | setsid 17085 |
. . . . . 6
β’ ((π β V β§ (π΄ β© π΅) β V) β (π΄ β© π΅) = (Baseβ(π sSet β¨(Baseβndx), (π΄ β© π΅)β©))) |
15 | 10, 12, 14 | sylancl 587 |
. . . . 5
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β π) β (π΄ β© π΅) = (Baseβ(π sSet β¨(Baseβndx), (π΄ β© π΅)β©))) |
16 | 5, 1 | ressval2 17122 |
. . . . . 6
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β π) β π
= (π sSet β¨(Baseβndx), (π΄ β© π΅)β©)) |
17 | 16 | fveq2d 6847 |
. . . . 5
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β π) β (Baseβπ
) = (Baseβ(π sSet β¨(Baseβndx), (π΄ β© π΅)β©))) |
18 | 15, 17 | eqtr4d 2776 |
. . . 4
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β π) β (π΄ β© π΅) = (Baseβπ
)) |
19 | 18 | 3expib 1123 |
. . 3
β’ (Β¬
π΅ β π΄ β ((π β V β§ π΄ β π) β (π΄ β© π΅) = (Baseβπ
))) |
20 | 9, 19 | pm2.61i 182 |
. 2
β’ ((π β V β§ π΄ β π) β (π΄ β© π΅) = (Baseβπ
)) |
21 | | 0fv 6887 |
. . . . 5
β’
(β
β(Baseβndx)) = β
|
22 | | 0ex 5265 |
. . . . . 6
β’ β
β V |
23 | 22, 13 | strfvn 17063 |
. . . . 5
β’
(Baseββ
) = (β
β(Baseβndx)) |
24 | | in0 4352 |
. . . . 5
β’ (π΄ β© β
) =
β
|
25 | 21, 23, 24 | 3eqtr4ri 2772 |
. . . 4
β’ (π΄ β© β
) =
(Baseββ
) |
26 | | fvprc 6835 |
. . . . . 6
β’ (Β¬
π β V β
(Baseβπ) =
β
) |
27 | 1, 26 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π β V β π΅ = β
) |
28 | 27 | ineq2d 4173 |
. . . 4
β’ (Β¬
π β V β (π΄ β© π΅) = (π΄ β© β
)) |
29 | | reldmress 17119 |
. . . . . . 7
β’ Rel dom
βΎs |
30 | 29 | ovprc1 7397 |
. . . . . 6
β’ (Β¬
π β V β (π βΎs π΄) = β
) |
31 | 5, 30 | eqtrid 2785 |
. . . . 5
β’ (Β¬
π β V β π
= β
) |
32 | 31 | fveq2d 6847 |
. . . 4
β’ (Β¬
π β V β
(Baseβπ
) =
(Baseββ
)) |
33 | 25, 28, 32 | 3eqtr4a 2799 |
. . 3
β’ (Β¬
π β V β (π΄ β© π΅) = (Baseβπ
)) |
34 | 33 | adantr 482 |
. 2
β’ ((Β¬
π β V β§ π΄ β π) β (π΄ β© π΅) = (Baseβπ
)) |
35 | 20, 34 | pm2.61ian 811 |
1
β’ (π΄ β π β (π΄ β© π΅) = (Baseβπ
)) |