![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neiptopuni | Structured version Visualization version GIF version |
Description: Lemma for neiptopreu 22484. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
Ref | Expression |
---|---|
neiptop.o | ⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} |
neiptop.0 | ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) |
neiptop.1 | ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) |
neiptop.2 | ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) |
neiptop.3 | ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) |
neiptop.4 | ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) |
neiptop.5 | ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) |
Ref | Expression |
---|---|
neiptopuni | ⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpwi 4567 | . . . . . . . 8 ⊢ (𝑎 ∈ 𝒫 𝑋 → 𝑎 ⊆ 𝑋) | |
2 | 1 | ad2antlr 725 | . . . . . . 7 ⊢ (((𝑝 ∈ ∪ 𝐽 ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑎 ⊆ 𝑋) |
3 | simpr 485 | . . . . . . 7 ⊢ (((𝑝 ∈ ∪ 𝐽 ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑝 ∈ 𝑎) | |
4 | 2, 3 | sseldd 3945 | . . . . . 6 ⊢ (((𝑝 ∈ ∪ 𝐽 ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑝 ∈ 𝑋) |
5 | neiptop.o | . . . . . . . . . 10 ⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} | |
6 | 5 | unieqi 4878 | . . . . . . . . 9 ⊢ ∪ 𝐽 = ∪ {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} |
7 | 6 | eleq2i 2829 | . . . . . . . 8 ⊢ (𝑝 ∈ ∪ 𝐽 ↔ 𝑝 ∈ ∪ {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}) |
8 | elunirab 4881 | . . . . . . . 8 ⊢ (𝑝 ∈ ∪ {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ↔ ∃𝑎 ∈ 𝒫 𝑋(𝑝 ∈ 𝑎 ∧ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝))) | |
9 | 7, 8 | bitri 274 | . . . . . . 7 ⊢ (𝑝 ∈ ∪ 𝐽 ↔ ∃𝑎 ∈ 𝒫 𝑋(𝑝 ∈ 𝑎 ∧ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝))) |
10 | simpl 483 | . . . . . . . 8 ⊢ ((𝑝 ∈ 𝑎 ∧ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) | |
11 | 10 | reximi 3087 | . . . . . . 7 ⊢ (∃𝑎 ∈ 𝒫 𝑋(𝑝 ∈ 𝑎 ∧ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑎 ∈ 𝒫 𝑋𝑝 ∈ 𝑎) |
12 | 9, 11 | sylbi 216 | . . . . . 6 ⊢ (𝑝 ∈ ∪ 𝐽 → ∃𝑎 ∈ 𝒫 𝑋𝑝 ∈ 𝑎) |
13 | 4, 12 | r19.29a 3159 | . . . . 5 ⊢ (𝑝 ∈ ∪ 𝐽 → 𝑝 ∈ 𝑋) |
14 | 13 | a1i 11 | . . . 4 ⊢ (𝜑 → (𝑝 ∈ ∪ 𝐽 → 𝑝 ∈ 𝑋)) |
15 | 14 | ssrdv 3950 | . . 3 ⊢ (𝜑 → ∪ 𝐽 ⊆ 𝑋) |
16 | ssidd 3967 | . . . 4 ⊢ (𝜑 → 𝑋 ⊆ 𝑋) | |
17 | neiptop.5 | . . . . 5 ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) | |
18 | 17 | ralrimiva 3143 | . . . 4 ⊢ (𝜑 → ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝)) |
19 | 5 | neipeltop 22480 | . . . 4 ⊢ (𝑋 ∈ 𝐽 ↔ (𝑋 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝑋 𝑋 ∈ (𝑁‘𝑝))) |
20 | 16, 18, 19 | sylanbrc 583 | . . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐽) |
21 | unissel 4899 | . . 3 ⊢ ((∪ 𝐽 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → ∪ 𝐽 = 𝑋) | |
22 | 15, 20, 21 | syl2anc 584 | . 2 ⊢ (𝜑 → ∪ 𝐽 = 𝑋) |
23 | 22 | eqcomd 2742 | 1 ⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3064 ∃wrex 3073 {crab 3407 ⊆ wss 3910 𝒫 cpw 4560 ∪ cuni 4865 ⟶wf 6492 ‘cfv 6496 ficfi 9346 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-nul 5263 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2944 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-in 3917 df-ss 3927 df-nul 4283 df-pw 4562 df-uni 4866 |
This theorem is referenced by: neiptoptop 22482 neiptopnei 22483 neiptopreu 22484 |
Copyright terms: Public domain | W3C validator |