Proof of Theorem diffiunisros
Step | Hyp | Ref
| Expression |
1 | | simp2 1139 |
. . 3
⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝐴 ∈ 𝑆) |
2 | | simp3 1140 |
. . 3
⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 𝐵 ∈ 𝑆) |
3 | | issros.1 |
. . . . . 6
⊢ 𝑁 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑠 ((𝑥 ∩ 𝑦) ∈ 𝑠 ∧ ∃𝑧 ∈ 𝒫 𝑠(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))} |
4 | 3 | issros 31855 |
. . . . 5
⊢ (𝑆 ∈ 𝑁 ↔ (𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ((𝑥 ∩ 𝑦) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)))) |
5 | 4 | simp3bi 1149 |
. . . 4
⊢ (𝑆 ∈ 𝑁 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ((𝑥 ∩ 𝑦) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧))) |
6 | 5 | 3ad2ant1 1135 |
. . 3
⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ((𝑥 ∩ 𝑦) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧))) |
7 | | ineq1 4120 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝑦) = (𝐴 ∩ 𝑦)) |
8 | 7 | eleq1d 2822 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝑦) ∈ 𝑆 ↔ (𝐴 ∩ 𝑦) ∈ 𝑆)) |
9 | | difeq1 4030 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 ∖ 𝑦) = (𝐴 ∖ 𝑦)) |
10 | 9 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑥 ∖ 𝑦) = ∪ 𝑧 ↔ (𝐴 ∖ 𝑦) = ∪ 𝑧)) |
11 | 10 | 3anbi3d 1444 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧) ↔ (𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝑦) = ∪ 𝑧))) |
12 | 11 | rexbidv 3216 |
. . . . 5
⊢ (𝑥 = 𝐴 → (∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧) ↔ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝑦) = ∪ 𝑧))) |
13 | 8, 12 | anbi12d 634 |
. . . 4
⊢ (𝑥 = 𝐴 → (((𝑥 ∩ 𝑦) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧)) ↔ ((𝐴 ∩ 𝑦) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝑦) = ∪ 𝑧)))) |
14 | | ineq2 4121 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝐴 ∩ 𝑦) = (𝐴 ∩ 𝐵)) |
15 | 14 | eleq1d 2822 |
. . . . 5
⊢ (𝑦 = 𝐵 → ((𝐴 ∩ 𝑦) ∈ 𝑆 ↔ (𝐴 ∩ 𝐵) ∈ 𝑆)) |
16 | | difeq2 4031 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝐴 ∖ 𝑦) = (𝐴 ∖ 𝐵)) |
17 | 16 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → ((𝐴 ∖ 𝑦) = ∪ 𝑧 ↔ (𝐴 ∖ 𝐵) = ∪ 𝑧)) |
18 | 17 | 3anbi3d 1444 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝑦) = ∪ 𝑧) ↔ (𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝐵) = ∪ 𝑧))) |
19 | 18 | rexbidv 3216 |
. . . . 5
⊢ (𝑦 = 𝐵 → (∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝑦) = ∪ 𝑧) ↔ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝐵) = ∪ 𝑧))) |
20 | 15, 19 | anbi12d 634 |
. . . 4
⊢ (𝑦 = 𝐵 → (((𝐴 ∩ 𝑦) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝑦) = ∪ 𝑧)) ↔ ((𝐴 ∩ 𝐵) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝐵) = ∪ 𝑧)))) |
21 | 13, 20 | rspc2va 3548 |
. . 3
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ((𝑥 ∩ 𝑦) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝑥 ∖ 𝑦) = ∪ 𝑧))) → ((𝐴 ∩ 𝐵) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝐵) = ∪ 𝑧))) |
22 | 1, 2, 6, 21 | syl21anc 838 |
. 2
⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴 ∩ 𝐵) ∈ 𝑆 ∧ ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝐵) = ∪ 𝑧))) |
23 | 22 | simprd 499 |
1
⊢ ((𝑆 ∈ 𝑁 ∧ 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ∃𝑧 ∈ 𝒫 𝑆(𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ (𝐴 ∖ 𝐵) = ∪ 𝑧)) |