Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . . . . . . 9
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β Β¬ (Baseβπ) β π΄) |
2 | | simpr1 1195 |
. . . . . . . . 9
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β π β V) |
3 | | simpr2 1196 |
. . . . . . . . 9
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β π΄ β π) |
4 | | eqid 2733 |
. . . . . . . . . 10
β’ (π βΎs π΄) = (π βΎs π΄) |
5 | | eqid 2733 |
. . . . . . . . . 10
β’
(Baseβπ) =
(Baseβπ) |
6 | 4, 5 | ressval2 17122 |
. . . . . . . . 9
β’ ((Β¬
(Baseβπ) β
π΄ β§ π β V β§ π΄ β π) β (π βΎs π΄) = (π sSet β¨(Baseβndx), (π΄ β© (Baseβπ))β©)) |
7 | 1, 2, 3, 6 | syl3anc 1372 |
. . . . . . . 8
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π βΎs π΄) = (π sSet β¨(Baseβndx), (π΄ β© (Baseβπ))β©)) |
8 | | inass 4180 |
. . . . . . . . . . 11
β’ ((π΄ β© π΅) β© (Baseβπ)) = (π΄ β© (π΅ β© (Baseβπ))) |
9 | | in12 4181 |
. . . . . . . . . . 11
β’ (π΄ β© (π΅ β© (Baseβπ))) = (π΅ β© (π΄ β© (Baseβπ))) |
10 | 8, 9 | eqtri 2761 |
. . . . . . . . . 10
β’ ((π΄ β© π΅) β© (Baseβπ)) = (π΅ β© (π΄ β© (Baseβπ))) |
11 | 4, 5 | ressbas 17123 |
. . . . . . . . . . . 12
β’ (π΄ β π β (π΄ β© (Baseβπ)) = (Baseβ(π βΎs π΄))) |
12 | 3, 11 | syl 17 |
. . . . . . . . . . 11
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π΄ β© (Baseβπ)) = (Baseβ(π βΎs π΄))) |
13 | 12 | ineq2d 4173 |
. . . . . . . . . 10
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π΅ β© (π΄ β© (Baseβπ))) = (π΅ β© (Baseβ(π βΎs π΄)))) |
14 | 10, 13 | eqtr2id 2786 |
. . . . . . . . 9
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π΅ β© (Baseβ(π βΎs π΄))) = ((π΄ β© π΅) β© (Baseβπ))) |
15 | 14 | opeq2d 4838 |
. . . . . . . 8
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β β¨(Baseβndx), (π΅ β© (Baseβ(π βΎs π΄)))β© =
β¨(Baseβndx), ((π΄
β© π΅) β©
(Baseβπ))β©) |
16 | 7, 15 | oveq12d 7376 |
. . . . . . 7
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β ((π βΎs π΄) sSet β¨(Baseβndx), (π΅ β© (Baseβ(π βΎs π΄)))β©) = ((π sSet β¨(Baseβndx), (π΄ β© (Baseβπ))β©) sSet
β¨(Baseβndx), ((π΄
β© π΅) β©
(Baseβπ))β©)) |
17 | | fvex 6856 |
. . . . . . . . 9
β’
(Baseβπ)
β V |
18 | 17 | inex2 5276 |
. . . . . . . 8
β’ ((π΄ β© π΅) β© (Baseβπ)) β V |
19 | | setsabs 17056 |
. . . . . . . 8
β’ ((π β V β§ ((π΄ β© π΅) β© (Baseβπ)) β V) β ((π sSet β¨(Baseβndx), (π΄ β© (Baseβπ))β©) sSet
β¨(Baseβndx), ((π΄
β© π΅) β©
(Baseβπ))β©) =
(π sSet
β¨(Baseβndx), ((π΄
β© π΅) β©
(Baseβπ))β©)) |
20 | 2, 18, 19 | sylancl 587 |
. . . . . . 7
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β ((π sSet β¨(Baseβndx), (π΄ β© (Baseβπ))β©) sSet
β¨(Baseβndx), ((π΄
β© π΅) β©
(Baseβπ))β©) =
(π sSet
β¨(Baseβndx), ((π΄
β© π΅) β©
(Baseβπ))β©)) |
21 | 16, 20 | eqtrd 2773 |
. . . . . 6
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β ((π βΎs π΄) sSet β¨(Baseβndx), (π΅ β© (Baseβ(π βΎs π΄)))β©) = (π sSet β¨(Baseβndx), ((π΄ β© π΅) β© (Baseβπ))β©)) |
22 | | simpll 766 |
. . . . . . 7
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β Β¬ (Baseβ(π βΎs π΄)) β π΅) |
23 | | ovexd 7393 |
. . . . . . 7
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π βΎs π΄) β V) |
24 | | simpr3 1197 |
. . . . . . 7
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β π΅ β π) |
25 | | eqid 2733 |
. . . . . . . 8
β’ ((π βΎs π΄) βΎs π΅) = ((π βΎs π΄) βΎs π΅) |
26 | | eqid 2733 |
. . . . . . . 8
β’
(Baseβ(π
βΎs π΄)) =
(Baseβ(π
βΎs π΄)) |
27 | 25, 26 | ressval2 17122 |
. . . . . . 7
β’ ((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ (π βΎs π΄) β V β§ π΅ β π) β ((π βΎs π΄) βΎs π΅) = ((π βΎs π΄) sSet β¨(Baseβndx), (π΅ β© (Baseβ(π βΎs π΄)))β©)) |
28 | 22, 23, 24, 27 | syl3anc 1372 |
. . . . . 6
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β ((π βΎs π΄) βΎs π΅) = ((π βΎs π΄) sSet β¨(Baseβndx), (π΅ β© (Baseβ(π βΎs π΄)))β©)) |
29 | | inss1 4189 |
. . . . . . . . 9
β’ (π΄ β© π΅) β π΄ |
30 | | sstr 3953 |
. . . . . . . . 9
β’
(((Baseβπ)
β (π΄ β© π΅) β§ (π΄ β© π΅) β π΄) β (Baseβπ) β π΄) |
31 | 29, 30 | mpan2 690 |
. . . . . . . 8
β’
((Baseβπ)
β (π΄ β© π΅) β (Baseβπ) β π΄) |
32 | 1, 31 | nsyl 140 |
. . . . . . 7
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β Β¬ (Baseβπ) β (π΄ β© π΅)) |
33 | | inex1g 5277 |
. . . . . . . 8
β’ (π΄ β π β (π΄ β© π΅) β V) |
34 | 3, 33 | syl 17 |
. . . . . . 7
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π΄ β© π΅) β V) |
35 | | eqid 2733 |
. . . . . . . 8
β’ (π βΎs (π΄ β© π΅)) = (π βΎs (π΄ β© π΅)) |
36 | 35, 5 | ressval2 17122 |
. . . . . . 7
β’ ((Β¬
(Baseβπ) β
(π΄ β© π΅) β§ π β V β§ (π΄ β© π΅) β V) β (π βΎs (π΄ β© π΅)) = (π sSet β¨(Baseβndx), ((π΄ β© π΅) β© (Baseβπ))β©)) |
37 | 32, 2, 34, 36 | syl3anc 1372 |
. . . . . 6
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π βΎs (π΄ β© π΅)) = (π sSet β¨(Baseβndx), ((π΄ β© π΅) β© (Baseβπ))β©)) |
38 | 21, 28, 37 | 3eqtr4d 2783 |
. . . . 5
β’ (((Β¬
(Baseβ(π
βΎs π΄))
β π΅ β§ Β¬
(Baseβπ) β
π΄) β§ (π β V β§ π΄ β π β§ π΅ β π)) β ((π βΎs π΄) βΎs π΅) = (π βΎs (π΄ β© π΅))) |
39 | 38 | exp31 421 |
. . . 4
β’ (Β¬
(Baseβ(π
βΎs π΄))
β π΅ β (Β¬
(Baseβπ) β
π΄ β ((π β V β§ π΄ β π β§ π΅ β π) β ((π βΎs π΄) βΎs π΅) = (π βΎs (π΄ β© π΅))))) |
40 | | ovex 7391 |
. . . . . . . 8
β’ (π βΎs π΄) β V |
41 | 25, 26 | ressid2 17121 |
. . . . . . . 8
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π βΎs π΄) β V β§ π΅ β π) β ((π βΎs π΄) βΎs π΅) = (π βΎs π΄)) |
42 | 40, 41 | mp3an2 1450 |
. . . . . . 7
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ π΅ β π) β ((π βΎs π΄) βΎs π΅) = (π βΎs π΄)) |
43 | 42 | 3ad2antr3 1191 |
. . . . . 6
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π β V β§ π΄ β π β§ π΅ β π)) β ((π βΎs π΄) βΎs π΅) = (π βΎs π΄)) |
44 | | in32 4182 |
. . . . . . . . 9
β’ ((π΄ β© π΅) β© (Baseβπ)) = ((π΄ β© (Baseβπ)) β© π΅) |
45 | | simpr2 1196 |
. . . . . . . . . . . 12
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π β V β§ π΄ β π β§ π΅ β π)) β π΄ β π) |
46 | 45, 11 | syl 17 |
. . . . . . . . . . 11
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π΄ β© (Baseβπ)) = (Baseβ(π βΎs π΄))) |
47 | | simpl 484 |
. . . . . . . . . . 11
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (Baseβ(π βΎs π΄)) β π΅) |
48 | 46, 47 | eqsstrd 3983 |
. . . . . . . . . 10
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π΄ β© (Baseβπ)) β π΅) |
49 | | df-ss 3928 |
. . . . . . . . . 10
β’ ((π΄ β© (Baseβπ)) β π΅ β ((π΄ β© (Baseβπ)) β© π΅) = (π΄ β© (Baseβπ))) |
50 | 48, 49 | sylib 217 |
. . . . . . . . 9
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π β V β§ π΄ β π β§ π΅ β π)) β ((π΄ β© (Baseβπ)) β© π΅) = (π΄ β© (Baseβπ))) |
51 | 44, 50 | eqtr2id 2786 |
. . . . . . . 8
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π΄ β© (Baseβπ)) = ((π΄ β© π΅) β© (Baseβπ))) |
52 | 51 | oveq2d 7374 |
. . . . . . 7
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π βΎs (π΄ β© (Baseβπ))) = (π βΎs ((π΄ β© π΅) β© (Baseβπ)))) |
53 | 5 | ressinbas 17131 |
. . . . . . . 8
β’ (π΄ β π β (π βΎs π΄) = (π βΎs (π΄ β© (Baseβπ)))) |
54 | 45, 53 | syl 17 |
. . . . . . 7
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π βΎs π΄) = (π βΎs (π΄ β© (Baseβπ)))) |
55 | 5 | ressinbas 17131 |
. . . . . . . 8
β’ ((π΄ β© π΅) β V β (π βΎs (π΄ β© π΅)) = (π βΎs ((π΄ β© π΅) β© (Baseβπ)))) |
56 | 45, 33, 55 | 3syl 18 |
. . . . . . 7
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π βΎs (π΄ β© π΅)) = (π βΎs ((π΄ β© π΅) β© (Baseβπ)))) |
57 | 52, 54, 56 | 3eqtr4d 2783 |
. . . . . 6
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π βΎs π΄) = (π βΎs (π΄ β© π΅))) |
58 | 43, 57 | eqtrd 2773 |
. . . . 5
β’
(((Baseβ(π
βΎs π΄))
β π΅ β§ (π β V β§ π΄ β π β§ π΅ β π)) β ((π βΎs π΄) βΎs π΅) = (π βΎs (π΄ β© π΅))) |
59 | 58 | ex 414 |
. . . 4
β’
((Baseβ(π
βΎs π΄))
β π΅ β ((π β V β§ π΄ β π β§ π΅ β π) β ((π βΎs π΄) βΎs π΅) = (π βΎs (π΄ β© π΅)))) |
60 | 4, 5 | ressid2 17121 |
. . . . . . . 8
β’
(((Baseβπ)
β π΄ β§ π β V β§ π΄ β π) β (π βΎs π΄) = π) |
61 | 60 | 3adant3r3 1185 |
. . . . . . 7
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π βΎs π΄) = π) |
62 | 61 | oveq1d 7373 |
. . . . . 6
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β ((π βΎs π΄) βΎs π΅) = (π βΎs π΅)) |
63 | | inss2 4190 |
. . . . . . . . . . 11
β’ (π΅ β© (Baseβπ)) β (Baseβπ) |
64 | | simpl 484 |
. . . . . . . . . . 11
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (Baseβπ) β π΄) |
65 | 63, 64 | sstrid 3956 |
. . . . . . . . . 10
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π΅ β© (Baseβπ)) β π΄) |
66 | | sseqin2 4176 |
. . . . . . . . . 10
β’ ((π΅ β© (Baseβπ)) β π΄ β (π΄ β© (π΅ β© (Baseβπ))) = (π΅ β© (Baseβπ))) |
67 | 65, 66 | sylib 217 |
. . . . . . . . 9
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π΄ β© (π΅ β© (Baseβπ))) = (π΅ β© (Baseβπ))) |
68 | 8, 67 | eqtr2id 2786 |
. . . . . . . 8
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π΅ β© (Baseβπ)) = ((π΄ β© π΅) β© (Baseβπ))) |
69 | 68 | oveq2d 7374 |
. . . . . . 7
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π βΎs (π΅ β© (Baseβπ))) = (π βΎs ((π΄ β© π΅) β© (Baseβπ)))) |
70 | | simpr3 1197 |
. . . . . . . 8
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β π΅ β π) |
71 | 5 | ressinbas 17131 |
. . . . . . . 8
β’ (π΅ β π β (π βΎs π΅) = (π βΎs (π΅ β© (Baseβπ)))) |
72 | 70, 71 | syl 17 |
. . . . . . 7
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π βΎs π΅) = (π βΎs (π΅ β© (Baseβπ)))) |
73 | | simpr2 1196 |
. . . . . . . 8
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β π΄ β π) |
74 | 73, 33, 55 | 3syl 18 |
. . . . . . 7
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π βΎs (π΄ β© π΅)) = (π βΎs ((π΄ β© π΅) β© (Baseβπ)))) |
75 | 69, 72, 74 | 3eqtr4d 2783 |
. . . . . 6
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β (π βΎs π΅) = (π βΎs (π΄ β© π΅))) |
76 | 62, 75 | eqtrd 2773 |
. . . . 5
β’
(((Baseβπ)
β π΄ β§ (π β V β§ π΄ β π β§ π΅ β π)) β ((π βΎs π΄) βΎs π΅) = (π βΎs (π΄ β© π΅))) |
77 | 76 | ex 414 |
. . . 4
β’
((Baseβπ)
β π΄ β ((π β V β§ π΄ β π β§ π΅ β π) β ((π βΎs π΄) βΎs π΅) = (π βΎs (π΄ β© π΅)))) |
78 | 39, 59, 77 | pm2.61ii 183 |
. . 3
β’ ((π β V β§ π΄ β π β§ π΅ β π) β ((π βΎs π΄) βΎs π΅) = (π βΎs (π΄ β© π΅))) |
79 | 78 | 3expib 1123 |
. 2
β’ (π β V β ((π΄ β π β§ π΅ β π) β ((π βΎs π΄) βΎs π΅) = (π βΎs (π΄ β© π΅)))) |
80 | | ress0 17129 |
. . . 4
β’ (β
βΎs π΅) =
β
|
81 | | reldmress 17119 |
. . . . . 6
β’ Rel dom
βΎs |
82 | 81 | ovprc1 7397 |
. . . . 5
β’ (Β¬
π β V β (π βΎs π΄) = β
) |
83 | 82 | oveq1d 7373 |
. . . 4
β’ (Β¬
π β V β ((π βΎs π΄) βΎs π΅) = (β
βΎs
π΅)) |
84 | 81 | ovprc1 7397 |
. . . 4
β’ (Β¬
π β V β (π βΎs (π΄ β© π΅)) = β
) |
85 | 80, 83, 84 | 3eqtr4a 2799 |
. . 3
β’ (Β¬
π β V β ((π βΎs π΄) βΎs π΅) = (π βΎs (π΄ β© π΅))) |
86 | 85 | a1d 25 |
. 2
β’ (Β¬
π β V β ((π΄ β π β§ π΅ β π) β ((π βΎs π΄) βΎs π΅) = (π βΎs (π΄ β© π΅)))) |
87 | 79, 86 | pm2.61i 182 |
1
β’ ((π΄ β π β§ π΅ β π) β ((π βΎs π΄) βΎs π΅) = (π βΎs (π΄ β© π΅))) |