Proof of Theorem intabs
| Step | Hyp | Ref
| Expression |
| 1 | | sseq1 4009 |
. . . . . 6
⊢ (𝑥 = ∩
{𝑦 ∣ 𝜓} → (𝑥 ⊆ 𝐴 ↔ ∩ {𝑦 ∣ 𝜓} ⊆ 𝐴)) |
| 2 | | intabs.2 |
. . . . . 6
⊢ (𝑥 = ∩
{𝑦 ∣ 𝜓} → (𝜑 ↔ 𝜒)) |
| 3 | 1, 2 | anbi12d 632 |
. . . . 5
⊢ (𝑥 = ∩
{𝑦 ∣ 𝜓} → ((𝑥 ⊆ 𝐴 ∧ 𝜑) ↔ (∩
{𝑦 ∣ 𝜓} ⊆ 𝐴 ∧ 𝜒))) |
| 4 | | intabs.3 |
. . . . 5
⊢ (∩ {𝑦
∣ 𝜓} ⊆ 𝐴 ∧ 𝜒) |
| 5 | 3, 4 | intmin3 4976 |
. . . 4
⊢ (∩ {𝑦
∣ 𝜓} ∈ V →
∩ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ⊆ ∩
{𝑦 ∣ 𝜓}) |
| 6 | | intnex 5345 |
. . . . 5
⊢ (¬
∩ {𝑦 ∣ 𝜓} ∈ V ↔ ∩ {𝑦
∣ 𝜓} =
V) |
| 7 | | ssv 4008 |
. . . . . 6
⊢ ∩ {𝑥
∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ⊆ V |
| 8 | | sseq2 4010 |
. . . . . 6
⊢ (∩ {𝑦
∣ 𝜓} = V → (∩ {𝑥
∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ⊆ ∩
{𝑦 ∣ 𝜓} ↔ ∩ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ⊆ V)) |
| 9 | 7, 8 | mpbiri 258 |
. . . . 5
⊢ (∩ {𝑦
∣ 𝜓} = V → ∩ {𝑥
∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ⊆ ∩
{𝑦 ∣ 𝜓}) |
| 10 | 6, 9 | sylbi 217 |
. . . 4
⊢ (¬
∩ {𝑦 ∣ 𝜓} ∈ V → ∩ {𝑥
∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ⊆ ∩
{𝑦 ∣ 𝜓}) |
| 11 | 5, 10 | pm2.61i 182 |
. . 3
⊢ ∩ {𝑥
∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ⊆ ∩
{𝑦 ∣ 𝜓} |
| 12 | | intabs.1 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
| 13 | 12 | cbvabv 2812 |
. . . 4
⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} |
| 14 | 13 | inteqi 4950 |
. . 3
⊢ ∩ {𝑥
∣ 𝜑} = ∩ {𝑦
∣ 𝜓} |
| 15 | 11, 14 | sseqtrri 4033 |
. 2
⊢ ∩ {𝑥
∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ⊆ ∩
{𝑥 ∣ 𝜑} |
| 16 | | simpr 484 |
. . . 4
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝜑) → 𝜑) |
| 17 | 16 | ss2abi 4067 |
. . 3
⊢ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ 𝜑} |
| 18 | | intss 4969 |
. . 3
⊢ ({𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} ⊆ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ 𝜑} ⊆ ∩
{𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)}) |
| 19 | 17, 18 | ax-mp 5 |
. 2
⊢ ∩ {𝑥
∣ 𝜑} ⊆ ∩ {𝑥
∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} |
| 20 | 15, 19 | eqssi 4000 |
1
⊢ ∩ {𝑥
∣ (𝑥 ⊆ 𝐴 ∧ 𝜑)} = ∩ {𝑥 ∣ 𝜑} |