Step | Hyp | Ref
| Expression |
1 | | intsaluni.gn0 |
. . 3
⊢ (𝜑 → 𝐺 ≠ ∅) |
2 | | n0 3931 |
. . . 4
⊢ (𝐺 ≠ ∅ ↔
∃𝑠 𝑠 ∈ 𝐺) |
3 | 2 | biimpi 206 |
. . 3
⊢ (𝐺 ≠ ∅ →
∃𝑠 𝑠 ∈ 𝐺) |
4 | 1, 3 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑠 𝑠 ∈ 𝐺) |
5 | | nfv 1843 |
. . 3
⊢
Ⅎ𝑠𝜑 |
6 | | nfv 1843 |
. . 3
⊢
Ⅎ𝑠∪ ∩ 𝐺 = 𝑋 |
7 | | intss1 4492 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝐺 → ∩ 𝐺 ⊆ 𝑠) |
8 | | uniss 4458 |
. . . . . . . 8
⊢ (∩ 𝐺
⊆ 𝑠 → ∪ ∩ 𝐺 ⊆ ∪ 𝑠) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝑠 ∈ 𝐺 → ∪ ∩ 𝐺
⊆ ∪ 𝑠) |
10 | 9 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ ∩ 𝐺
⊆ ∪ 𝑠) |
11 | | intsaluni.x |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋) |
12 | 10, 11 | sseqtrd 3641 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ ∩ 𝐺
⊆ 𝑋) |
13 | 11 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐺) ∧ 𝑡 ∈ 𝐺) → ∪ 𝑠 = 𝑋) |
14 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑡 → (𝑠 ∈ 𝐺 ↔ 𝑡 ∈ 𝐺)) |
15 | 14 | anbi2d 740 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = 𝑡 → ((𝜑 ∧ 𝑠 ∈ 𝐺) ↔ (𝜑 ∧ 𝑡 ∈ 𝐺))) |
16 | | unieq 4444 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 𝑡 → ∪ 𝑠 = ∪
𝑡) |
17 | 16 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = 𝑡 → (∪ 𝑠 = 𝑋 ↔ ∪ 𝑡 = 𝑋)) |
18 | 15, 17 | imbi12d 334 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = 𝑡 → (((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 = 𝑋) ↔ ((𝜑 ∧ 𝑡 ∈ 𝐺) → ∪ 𝑡 = 𝑋))) |
19 | 18, 11 | chvarv 2263 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐺) → ∪ 𝑡 = 𝑋) |
20 | 19 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐺) → 𝑋 = ∪ 𝑡) |
21 | 20 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐺) ∧ 𝑡 ∈ 𝐺) → 𝑋 = ∪ 𝑡) |
22 | 13, 21 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐺) ∧ 𝑡 ∈ 𝐺) → ∪ 𝑠 = ∪
𝑡) |
23 | | intsaluni.ga |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺 ⊆ SAlg) |
24 | 23 | sselda 3603 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐺) → 𝑡 ∈ SAlg) |
25 | | saluni 40544 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ∈ SAlg → ∪ 𝑡
∈ 𝑡) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐺) → ∪ 𝑡 ∈ 𝑡) |
27 | 26 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐺) ∧ 𝑡 ∈ 𝐺) → ∪ 𝑡 ∈ 𝑡) |
28 | 22, 27 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐺) ∧ 𝑡 ∈ 𝐺) → ∪ 𝑠 ∈ 𝑡) |
29 | 28 | ralrimiva 2966 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∀𝑡 ∈ 𝐺 ∪ 𝑠 ∈ 𝑡) |
30 | | uniexg 6955 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ 𝐺 → ∪ 𝑠 ∈ V) |
31 | 30 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 ∈ V) |
32 | | elintg 4483 |
. . . . . . . . . . . 12
⊢ (∪ 𝑠
∈ V → (∪ 𝑠 ∈ ∩ 𝐺 ↔ ∀𝑡 ∈ 𝐺 ∪ 𝑠 ∈ 𝑡)) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → (∪ 𝑠 ∈ ∩ 𝐺
↔ ∀𝑡 ∈
𝐺 ∪ 𝑠
∈ 𝑡)) |
34 | 29, 33 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ 𝑠 ∈ ∩ 𝐺) |
35 | 34 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐺) ∧ 𝑥 ∈ 𝑋) → ∪ 𝑠 ∈ ∩ 𝐺) |
36 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
37 | 11 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝑋 = ∪ 𝑠) |
38 | 37 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑋 = ∪ 𝑠) |
39 | 36, 38 | eleqtrd 2703 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ∪ 𝑠) |
40 | | eleq2 2690 |
. . . . . . . . . 10
⊢ (𝑦 = ∪
𝑠 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ∪ 𝑠)) |
41 | 40 | rspcev 3309 |
. . . . . . . . 9
⊢ ((∪ 𝑠
∈ ∩ 𝐺 ∧ 𝑥 ∈ ∪ 𝑠) → ∃𝑦 ∈ ∩ 𝐺𝑥 ∈ 𝑦) |
42 | 35, 39, 41 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐺) ∧ 𝑥 ∈ 𝑋) → ∃𝑦 ∈ ∩ 𝐺𝑥 ∈ 𝑦) |
43 | | eluni2 4440 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ ∩ 𝐺 ↔ ∃𝑦 ∈ ∩ 𝐺𝑥 ∈ 𝑦) |
44 | 42, 43 | sylibr 224 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐺) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ∪ ∩ 𝐺) |
45 | 44 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ∩ 𝐺) |
46 | | dfss3 3592 |
. . . . . 6
⊢ (𝑋 ⊆ ∪ ∩ 𝐺 ↔ ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ∩ 𝐺) |
47 | 45, 46 | sylibr 224 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → 𝑋 ⊆ ∪ ∩ 𝐺) |
48 | 12, 47 | eqssd 3620 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐺) → ∪ ∩ 𝐺 =
𝑋) |
49 | 48 | ex 450 |
. . 3
⊢ (𝜑 → (𝑠 ∈ 𝐺 → ∪ ∩ 𝐺 =
𝑋)) |
50 | 5, 6, 49 | exlimd 2087 |
. 2
⊢ (𝜑 → (∃𝑠 𝑠 ∈ 𝐺 → ∪ ∩ 𝐺 =
𝑋)) |
51 | 4, 50 | mpd 15 |
1
⊢ (𝜑 → ∪ ∩ 𝐺 = 𝑋) |