Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝜑) |
2 | | intsal.ga |
. . . . . . 7
⊢ (𝜑 → 𝐺 ⊆ SAlg) |
3 | 2 | sselda 3921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg) |
4 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ SAlg) → 𝑠 ∈ SAlg) |
5 | | 0sal 43861 |
. . . . . . 7
⊢ (𝑠 ∈ SAlg → ∅
∈ 𝑠) |
6 | 4, 5 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ SAlg) → ∅ ∈ 𝑠) |
7 | 1, 3, 6 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∅ ∈ 𝑠) |
8 | 7 | ralrimiva 3103 |
. . . 4
⊢ (𝜑 → ∀𝑠 ∈ 𝐺 ∅ ∈ 𝑠) |
9 | | 0ex 5231 |
. . . . 5
⊢ ∅
∈ V |
10 | 9 | elint2 4886 |
. . . 4
⊢ (∅
∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∅ ∈ 𝑠) |
11 | 8, 10 | sylibr 233 |
. . 3
⊢ (𝜑 → ∅ ∈ ∩ 𝐺) |
12 | | intsal.x |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋) |
13 | | intsal.gn0 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ≠ ∅) |
14 | 2, 13, 12 | intsaluni 43868 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋) |
15 | 14 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 = ∪ ∩ 𝐺) |
16 | 15 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝑋 = ∪ ∩ 𝐺) |
17 | 12, 16 | eqtr2d 2779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ ∩ 𝐺 =
∪ 𝑠) |
18 | 17 | difeq1d 4056 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺
∖ 𝑦) = (∪ 𝑠
∖ 𝑦)) |
19 | 18 | adantlr 712 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺
∖ 𝑦) = (∪ 𝑠
∖ 𝑦)) |
20 | 3 | adantlr 712 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg) |
21 | | elinti 4888 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ∩ 𝐺
→ (𝑠 ∈ 𝐺 → 𝑦 ∈ 𝑠)) |
22 | 21 | imp 407 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ∩ 𝐺
∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝑠) |
23 | 22 | adantll 711 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝑠) |
24 | | saldifcl 43860 |
. . . . . . . 8
⊢ ((𝑠 ∈ SAlg ∧ 𝑦 ∈ 𝑠) → (∪ 𝑠 ∖ 𝑦) ∈ 𝑠) |
25 | 20, 23, 24 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ 𝑠 ∖ 𝑦) ∈ 𝑠) |
26 | 19, 25 | eqeltrd 2839 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) ∧ 𝑠 ∈ 𝐺) → (∪ ∩ 𝐺
∖ 𝑦) ∈ 𝑠) |
27 | 26 | ralrimiva 3103 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺
∖ 𝑦) ∈ 𝑠) |
28 | | intex 5261 |
. . . . . . . . . . 11
⊢ (𝐺 ≠ ∅ ↔ ∩ 𝐺
∈ V) |
29 | 28 | biimpi 215 |
. . . . . . . . . 10
⊢ (𝐺 ≠ ∅ → ∩ 𝐺
∈ V) |
30 | 13, 29 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ∩ 𝐺
∈ V) |
31 | 30 | uniexd 7595 |
. . . . . . . 8
⊢ (𝜑 → ∪ ∩ 𝐺 ∈ V) |
32 | 31 | difexd 5253 |
. . . . . . 7
⊢ (𝜑 → (∪ ∩ 𝐺 ∖ 𝑦) ∈ V) |
33 | 32 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ V) |
34 | | elintg 4887 |
. . . . . 6
⊢ ((∪ ∩ 𝐺 ∖ 𝑦) ∈ V → ((∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺
∖ 𝑦) ∈ 𝑠)) |
35 | 33, 34 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → ((∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 (∪ ∩ 𝐺
∖ 𝑦) ∈ 𝑠)) |
36 | 27, 35 | mpbird 256 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ∩ 𝐺) → (∪ ∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺) |
37 | 36 | ralrimiva 3103 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ ∩ 𝐺(∪
∩ 𝐺 ∖ 𝑦) ∈ ∩ 𝐺) |
38 | 3 | ad4ant14 749 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺)
∧ 𝑦 ≼ ω)
∧ 𝑠 ∈ 𝐺) → 𝑠 ∈ SAlg) |
39 | | elpwi 4542 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 ∩ 𝐺
→ 𝑦 ⊆ ∩ 𝐺) |
40 | 39 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺
∧ 𝑠 ∈ 𝐺) → 𝑦 ⊆ ∩ 𝐺) |
41 | | intss1 4894 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ 𝐺 → ∩ 𝐺 ⊆ 𝑠) |
42 | 41 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺
∧ 𝑠 ∈ 𝐺) → ∩ 𝐺
⊆ 𝑠) |
43 | 40, 42 | sstrd 3931 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺
∧ 𝑠 ∈ 𝐺) → 𝑦 ⊆ 𝑠) |
44 | | vex 3436 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
45 | 44 | elpw 4537 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 𝑠 ↔ 𝑦 ⊆ 𝑠) |
46 | 43, 45 | sylibr 233 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝒫 ∩ 𝐺
∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠) |
47 | 46 | adantll 711 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺)
∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠) |
48 | 47 | adantlr 712 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺)
∧ 𝑦 ≼ ω)
∧ 𝑠 ∈ 𝐺) → 𝑦 ∈ 𝒫 𝑠) |
49 | | simplr 766 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺)
∧ 𝑦 ≼ ω)
∧ 𝑠 ∈ 𝐺) → 𝑦 ≼ ω) |
50 | 38, 48, 49 | salunicl 43857 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺)
∧ 𝑦 ≼ ω)
∧ 𝑠 ∈ 𝐺) → ∪ 𝑦
∈ 𝑠) |
51 | 50 | ralrimiva 3103 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺)
∧ 𝑦 ≼ ω)
→ ∀𝑠 ∈
𝐺 ∪ 𝑦
∈ 𝑠) |
52 | | vuniex 7592 |
. . . . . . . 8
⊢ ∪ 𝑦
∈ V |
53 | 52 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺)
∧ 𝑦 ≼ ω)
→ ∪ 𝑦 ∈ V) |
54 | | elintg 4887 |
. . . . . . 7
⊢ (∪ 𝑦
∈ V → (∪ 𝑦 ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠)) |
55 | 53, 54 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺)
∧ 𝑦 ≼ ω)
→ (∪ 𝑦 ∈ ∩ 𝐺 ↔ ∀𝑠 ∈ 𝐺 ∪ 𝑦 ∈ 𝑠)) |
56 | 51, 55 | mpbird 256 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺)
∧ 𝑦 ≼ ω)
→ ∪ 𝑦 ∈ ∩ 𝐺) |
57 | 56 | ex 413 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ∩ 𝐺)
→ (𝑦 ≼ ω
→ ∪ 𝑦 ∈ ∩ 𝐺)) |
58 | 57 | ralrimiva 3103 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦
∈ ∩ 𝐺)) |
59 | 11, 37, 58 | 3jca 1127 |
. 2
⊢ (𝜑 → (∅ ∈ ∩ 𝐺
∧ ∀𝑦 ∈
∩ 𝐺(∪ ∩ 𝐺
∖ 𝑦) ∈ ∩ 𝐺
∧ ∀𝑦 ∈
𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦
∈ ∩ 𝐺))) |
60 | | issal 43855 |
. . 3
⊢ (∩ 𝐺
∈ V → (∩ 𝐺 ∈ SAlg ↔ (∅ ∈ ∩ 𝐺
∧ ∀𝑦 ∈
∩ 𝐺(∪ ∩ 𝐺
∖ 𝑦) ∈ ∩ 𝐺
∧ ∀𝑦 ∈
𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦
∈ ∩ 𝐺)))) |
61 | 30, 60 | syl 17 |
. 2
⊢ (𝜑 → (∩ 𝐺
∈ SAlg ↔ (∅ ∈ ∩ 𝐺 ∧ ∀𝑦 ∈ ∩ 𝐺(∪ ∩ 𝐺
∖ 𝑦) ∈ ∩ 𝐺
∧ ∀𝑦 ∈
𝒫 ∩ 𝐺(𝑦 ≼ ω → ∪ 𝑦
∈ ∩ 𝐺)))) |
62 | 59, 61 | mpbird 256 |
1
⊢ (𝜑 → ∩ 𝐺
∈ SAlg) |