Step | Hyp | Ref
| Expression |
1 | | elex 3492 |
. 2
β’ (π΄ β π β π΄ β V) |
2 | | eqid 2731 |
. . . . . . 7
β’ (π βΎs π΄) = (π βΎs π΄) |
3 | | ressid.1 |
. . . . . . 7
β’ π΅ = (Baseβπ) |
4 | 2, 3 | ressid2 17182 |
. . . . . 6
β’ ((π΅ β π΄ β§ π β V β§ π΄ β V) β (π βΎs π΄) = π) |
5 | | ssid 4004 |
. . . . . . . 8
β’ π΅ β π΅ |
6 | | incom 4201 |
. . . . . . . . 9
β’ (π΄ β© π΅) = (π΅ β© π΄) |
7 | | df-ss 3965 |
. . . . . . . . . 10
β’ (π΅ β π΄ β (π΅ β© π΄) = π΅) |
8 | 7 | biimpi 215 |
. . . . . . . . 9
β’ (π΅ β π΄ β (π΅ β© π΄) = π΅) |
9 | 6, 8 | eqtrid 2783 |
. . . . . . . 8
β’ (π΅ β π΄ β (π΄ β© π΅) = π΅) |
10 | 5, 9 | sseqtrrid 4035 |
. . . . . . 7
β’ (π΅ β π΄ β π΅ β (π΄ β© π΅)) |
11 | | elex 3492 |
. . . . . . 7
β’ (π β V β π β V) |
12 | | inex1g 5319 |
. . . . . . 7
β’ (π΄ β V β (π΄ β© π΅) β V) |
13 | | eqid 2731 |
. . . . . . . 8
β’ (π βΎs (π΄ β© π΅)) = (π βΎs (π΄ β© π΅)) |
14 | 13, 3 | ressid2 17182 |
. . . . . . 7
β’ ((π΅ β (π΄ β© π΅) β§ π β V β§ (π΄ β© π΅) β V) β (π βΎs (π΄ β© π΅)) = π) |
15 | 10, 11, 12, 14 | syl3an 1159 |
. . . . . 6
β’ ((π΅ β π΄ β§ π β V β§ π΄ β V) β (π βΎs (π΄ β© π΅)) = π) |
16 | 4, 15 | eqtr4d 2774 |
. . . . 5
β’ ((π΅ β π΄ β§ π β V β§ π΄ β V) β (π βΎs π΄) = (π βΎs (π΄ β© π΅))) |
17 | 16 | 3expb 1119 |
. . . 4
β’ ((π΅ β π΄ β§ (π β V β§ π΄ β V)) β (π βΎs π΄) = (π βΎs (π΄ β© π΅))) |
18 | | inass 4219 |
. . . . . . . . 9
β’ ((π΄ β© π΅) β© π΅) = (π΄ β© (π΅ β© π΅)) |
19 | | inidm 4218 |
. . . . . . . . . 10
β’ (π΅ β© π΅) = π΅ |
20 | 19 | ineq2i 4209 |
. . . . . . . . 9
β’ (π΄ β© (π΅ β© π΅)) = (π΄ β© π΅) |
21 | 18, 20 | eqtr2i 2760 |
. . . . . . . 8
β’ (π΄ β© π΅) = ((π΄ β© π΅) β© π΅) |
22 | 21 | opeq2i 4877 |
. . . . . . 7
β’
β¨(Baseβndx), (π΄ β© π΅)β© = β¨(Baseβndx), ((π΄ β© π΅) β© π΅)β© |
23 | 22 | oveq2i 7423 |
. . . . . 6
β’ (π sSet β¨(Baseβndx),
(π΄ β© π΅)β©) = (π sSet β¨(Baseβndx), ((π΄ β© π΅) β© π΅)β©) |
24 | 2, 3 | ressval2 17183 |
. . . . . 6
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β V) β (π βΎs π΄) = (π sSet β¨(Baseβndx), (π΄ β© π΅)β©)) |
25 | | inss1 4228 |
. . . . . . . . 9
β’ (π΄ β© π΅) β π΄ |
26 | | sstr 3990 |
. . . . . . . . 9
β’ ((π΅ β (π΄ β© π΅) β§ (π΄ β© π΅) β π΄) β π΅ β π΄) |
27 | 25, 26 | mpan2 688 |
. . . . . . . 8
β’ (π΅ β (π΄ β© π΅) β π΅ β π΄) |
28 | 27 | con3i 154 |
. . . . . . 7
β’ (Β¬
π΅ β π΄ β Β¬ π΅ β (π΄ β© π΅)) |
29 | 13, 3 | ressval2 17183 |
. . . . . . 7
β’ ((Β¬
π΅ β (π΄ β© π΅) β§ π β V β§ (π΄ β© π΅) β V) β (π βΎs (π΄ β© π΅)) = (π sSet β¨(Baseβndx), ((π΄ β© π΅) β© π΅)β©)) |
30 | 28, 11, 12, 29 | syl3an 1159 |
. . . . . 6
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β V) β (π βΎs (π΄ β© π΅)) = (π sSet β¨(Baseβndx), ((π΄ β© π΅) β© π΅)β©)) |
31 | 23, 24, 30 | 3eqtr4a 2797 |
. . . . 5
β’ ((Β¬
π΅ β π΄ β§ π β V β§ π΄ β V) β (π βΎs π΄) = (π βΎs (π΄ β© π΅))) |
32 | 31 | 3expb 1119 |
. . . 4
β’ ((Β¬
π΅ β π΄ β§ (π β V β§ π΄ β V)) β (π βΎs π΄) = (π βΎs (π΄ β© π΅))) |
33 | 17, 32 | pm2.61ian 809 |
. . 3
β’ ((π β V β§ π΄ β V) β (π βΎs π΄) = (π βΎs (π΄ β© π΅))) |
34 | | reldmress 17180 |
. . . . . 6
β’ Rel dom
βΎs |
35 | 34 | ovprc1 7451 |
. . . . 5
β’ (Β¬
π β V β (π βΎs π΄) = β
) |
36 | 34 | ovprc1 7451 |
. . . . 5
β’ (Β¬
π β V β (π βΎs (π΄ β© π΅)) = β
) |
37 | 35, 36 | eqtr4d 2774 |
. . . 4
β’ (Β¬
π β V β (π βΎs π΄) = (π βΎs (π΄ β© π΅))) |
38 | 37 | adantr 480 |
. . 3
β’ ((Β¬
π β V β§ π΄ β V) β (π βΎs π΄) = (π βΎs (π΄ β© π΅))) |
39 | 33, 38 | pm2.61ian 809 |
. 2
β’ (π΄ β V β (π βΎs π΄) = (π βΎs (π΄ β© π΅))) |
40 | 1, 39 | syl 17 |
1
β’ (π΄ β π β (π βΎs π΄) = (π βΎs (π΄ β© π΅))) |