Proof of Theorem op1stbg
Step | Hyp | Ref
| Expression |
1 | | dfopg 3538 |
. . . . 5
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → 〈A, B〉 =
{{A}, {A, B}}) |
2 | 1 | inteqd 3611 |
. . . 4
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → ∩ 〈A, B〉 = ∩ {{A}, {A, B}}) |
3 | | elex 2560 |
. . . . . . . 8
⊢ (A ∈ 𝑉 → A ∈
V) |
4 | | snexgOLD 3926 |
. . . . . . . 8
⊢ (A ∈ V →
{A} ∈
V) |
5 | 3, 4 | syl 14 |
. . . . . . 7
⊢ (A ∈ 𝑉 → {A} ∈
V) |
6 | 5 | adantr 261 |
. . . . . 6
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → {A} ∈
V) |
7 | | elex 2560 |
. . . . . . 7
⊢ (B ∈ 𝑊 → B ∈
V) |
8 | | prexgOLD 3937 |
. . . . . . 7
⊢
((A ∈ V ∧ B ∈ V) →
{A, B}
∈ V) |
9 | 3, 7, 8 | syl2an 273 |
. . . . . 6
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → {A, B} ∈ V) |
10 | | intprg 3639 |
. . . . . 6
⊢
(({A} ∈ V ∧ {A, B} ∈ V) → ∩ {{A}, {A, B}} = ({A} ∩
{A, B})) |
11 | 6, 9, 10 | syl2anc 391 |
. . . . 5
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → ∩ {{A}, {A, B}} =
({A} ∩ {A, B})) |
12 | | snsspr1 3503 |
. . . . . 6
⊢ {A} ⊆ {A,
B} |
13 | | df-ss 2925 |
. . . . . 6
⊢
({A} ⊆ {A, B} ↔
({A} ∩ {A, B}) =
{A}) |
14 | 12, 13 | mpbi 133 |
. . . . 5
⊢
({A} ∩ {A, B}) =
{A} |
15 | 11, 14 | syl6eq 2085 |
. . . 4
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → ∩ {{A}, {A, B}} =
{A}) |
16 | 2, 15 | eqtrd 2069 |
. . 3
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → ∩ 〈A, B〉 = {A}) |
17 | 16 | inteqd 3611 |
. 2
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → ∩ ∩ 〈A, B〉 =
∩ {A}) |
18 | | intsng 3640 |
. . 3
⊢ (A ∈ 𝑉 → ∩ {A} = A) |
19 | 18 | adantr 261 |
. 2
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → ∩ {A} = A) |
20 | 17, 19 | eqtrd 2069 |
1
⊢
((A ∈ 𝑉 ∧ B ∈ 𝑊) → ∩ ∩ 〈A, B〉 =
A) |