Proof of Theorem iinrab2
Step | Hyp | Ref
| Expression |
1 | | iineq1 4471 |
. . . . . 6
⊢ (𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = ∩
𝑥 ∈ ∅ {𝑦 ∈ 𝐵 ∣ 𝜑}) |
2 | | 0iin 4514 |
. . . . . 6
⊢ ∩ 𝑥 ∈ ∅ {𝑦 ∈ 𝐵 ∣ 𝜑} = V |
3 | 1, 2 | syl6eq 2660 |
. . . . 5
⊢ (𝐴 = ∅ → ∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = V) |
4 | 3 | ineq1d 3775 |
. . . 4
⊢ (𝐴 = ∅ → (∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} ∩ 𝐵) = (V ∩ 𝐵)) |
5 | | incom 3767 |
. . . . 5
⊢ (V ∩
𝐵) = (𝐵 ∩ V) |
6 | | inv1 3922 |
. . . . 5
⊢ (𝐵 ∩ V) = 𝐵 |
7 | 5, 6 | eqtri 2632 |
. . . 4
⊢ (V ∩
𝐵) = 𝐵 |
8 | 4, 7 | syl6eq 2660 |
. . 3
⊢ (𝐴 = ∅ → (∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} ∩ 𝐵) = 𝐵) |
9 | | rzal 4025 |
. . . 4
⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) |
10 | | rabid2 3096 |
. . . . 5
⊢ (𝐵 = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑} ↔ ∀𝑦 ∈ 𝐵 ∀𝑥 ∈ 𝐴 𝜑) |
11 | | ralcom 3079 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 ∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) |
12 | 10, 11 | bitr2i 264 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ 𝐵 = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑}) |
13 | 9, 12 | sylib 207 |
. . 3
⊢ (𝐴 = ∅ → 𝐵 = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑}) |
14 | 8, 13 | eqtrd 2644 |
. 2
⊢ (𝐴 = ∅ → (∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} ∩ 𝐵) = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑}) |
15 | | iinrab 4518 |
. . . 4
⊢ (𝐴 ≠ ∅ → ∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑}) |
16 | 15 | ineq1d 3775 |
. . 3
⊢ (𝐴 ≠ ∅ → (∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} ∩ 𝐵) = ({𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑} ∩ 𝐵)) |
17 | | ssrab2 3650 |
. . . 4
⊢ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑} ⊆ 𝐵 |
18 | | dfss 3555 |
. . . 4
⊢ ({𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑} ⊆ 𝐵 ↔ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑} = ({𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑} ∩ 𝐵)) |
19 | 17, 18 | mpbi 219 |
. . 3
⊢ {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑} = ({𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑} ∩ 𝐵) |
20 | 16, 19 | syl6eqr 2662 |
. 2
⊢ (𝐴 ≠ ∅ → (∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} ∩ 𝐵) = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑}) |
21 | 14, 20 | pm2.61ine 2865 |
1
⊢ (∩ 𝑥 ∈ 𝐴 {𝑦 ∈ 𝐵 ∣ 𝜑} ∩ 𝐵) = {𝑦 ∈ 𝐵 ∣ ∀𝑥 ∈ 𝐴 𝜑} |