Proof of Theorem op1stbg
Step | Hyp | Ref
| Expression |
1 | | dfopg 3547 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 〈𝐴, 𝐵〉 = {{𝐴}, {𝐴, 𝐵}}) |
2 | 1 | inteqd 3620 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩
〈𝐴, 𝐵〉 = ∩
{{𝐴}, {𝐴, 𝐵}}) |
3 | | elex 2566 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
4 | | snexgOLD 3935 |
. . . . . . . 8
⊢ (𝐴 ∈ V → {𝐴} ∈ V) |
5 | 3, 4 | syl 14 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) |
6 | 5 | adantr 261 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴} ∈ V) |
7 | | elex 2566 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) |
8 | | prexgOLD 3946 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V) |
9 | 3, 7, 8 | syl2an 273 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V) |
10 | | intprg 3648 |
. . . . . 6
⊢ (({𝐴} ∈ V ∧ {𝐴, 𝐵} ∈ V) → ∩ {{𝐴}, {𝐴, 𝐵}} = ({𝐴} ∩ {𝐴, 𝐵})) |
11 | 6, 9, 10 | syl2anc 391 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩
{{𝐴}, {𝐴, 𝐵}} = ({𝐴} ∩ {𝐴, 𝐵})) |
12 | | snsspr1 3512 |
. . . . . 6
⊢ {𝐴} ⊆ {𝐴, 𝐵} |
13 | | df-ss 2931 |
. . . . . 6
⊢ ({𝐴} ⊆ {𝐴, 𝐵} ↔ ({𝐴} ∩ {𝐴, 𝐵}) = {𝐴}) |
14 | 12, 13 | mpbi 133 |
. . . . 5
⊢ ({𝐴} ∩ {𝐴, 𝐵}) = {𝐴} |
15 | 11, 14 | syl6eq 2088 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩
{{𝐴}, {𝐴, 𝐵}} = {𝐴}) |
16 | 2, 15 | eqtrd 2072 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩
〈𝐴, 𝐵〉 = {𝐴}) |
17 | 16 | inteqd 3620 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ ∩ 〈𝐴, 𝐵〉 = ∩ {𝐴}) |
18 | | intsng 3649 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∩ {𝐴} = 𝐴) |
19 | 18 | adantr 261 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ {𝐴} = 𝐴) |
20 | 17, 19 | eqtrd 2072 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∩ ∩ 〈𝐴, 𝐵〉 = 𝐴) |