Metamath Proof Explorer

Theorem ntrneix13

Description: The closure of the union of any pair is equal to the union of closures if and only if the union of any pair belonging to the convergents of a point if equivalent to at least one of the pain belonging to the convergents of that point. (Contributed by RP, 19-Jun-2021)

Ref Expression
Hypotheses ntrnei.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
ntrnei.f ⊢ F = 𝒫 B O B
ntrnei.r ⊢ φ → I F N
Assertion ntrneix13 ⊢ φ → ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∪ t = I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ∪ t ∈ N ⁡ x ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢ O = i ∈ V , j ∈ V ⟼ k ∈ 𝒫 j i ⟼ l ∈ j ⟼ m ∈ i | l ∈ k ⁡ m
2 ntrnei.f ⊢ F = 𝒫 B O B
3 ntrnei.r ⊢ φ → I F N
4 dfss3 ⊢ I ⁡ s ∪ t ⊆ I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ I ⁡ s ∪ t x ∈ I ⁡ s ∪ I ⁡ t
5 1 2 3 ntrneiiex ⊢ φ → I ∈ 𝒫 B 𝒫 B
6 5 ad2antrr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ∈ 𝒫 B 𝒫 B
7 elmapi ⊢ I ∈ 𝒫 B 𝒫 B → I : 𝒫 B ⟶ 𝒫 B
8 6 7 syl ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I : 𝒫 B ⟶ 𝒫 B
9 1 2 3 ntrneibex ⊢ φ → B ∈ V
10 9 ad2antrr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → B ∈ V
11 simplr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → s ∈ 𝒫 B
12 11 elpwid ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → s ⊆ B
13 simpr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → t ∈ 𝒫 B
14 13 elpwid ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → t ⊆ B
15 12 14 unssd ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → s ∪ t ⊆ B
16 10 15 sselpwd ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → s ∪ t ∈ 𝒫 B
17 8 16 ffvelrnd ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ∪ t ∈ 𝒫 B
18 17 elpwid ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ∪ t ⊆ B
19 ralss ⊢ I ⁡ s ∪ t ⊆ B → ∀ x ∈ I ⁡ s ∪ t x ∈ I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∪ t → x ∈ I ⁡ s ∪ I ⁡ t
20 18 19 syl ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → ∀ x ∈ I ⁡ s ∪ t x ∈ I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∪ t → x ∈ I ⁡ s ∪ I ⁡ t
21 4 20 syl5bb ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ∪ t ⊆ I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∪ t → x ∈ I ⁡ s ∪ I ⁡ t
22 dfss3 ⊢ I ⁡ s ∪ I ⁡ t ⊆ I ⁡ s ∪ t ↔ ∀ x ∈ I ⁡ s ∪ I ⁡ t x ∈ I ⁡ s ∪ t
23 8 11 ffvelrnd ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ∈ 𝒫 B
24 23 elpwid ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ⊆ B
25 8 13 ffvelrnd ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ t ∈ 𝒫 B
26 25 elpwid ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ t ⊆ B
27 24 26 unssd ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ∪ I ⁡ t ⊆ B
28 ralss ⊢ I ⁡ s ∪ I ⁡ t ⊆ B → ∀ x ∈ I ⁡ s ∪ I ⁡ t x ∈ I ⁡ s ∪ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∪ I ⁡ t → x ∈ I ⁡ s ∪ t
29 27 28 syl ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → ∀ x ∈ I ⁡ s ∪ I ⁡ t x ∈ I ⁡ s ∪ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∪ I ⁡ t → x ∈ I ⁡ s ∪ t
30 22 29 syl5bb ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ∪ I ⁡ t ⊆ I ⁡ s ∪ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∪ I ⁡ t → x ∈ I ⁡ s ∪ t
31 21 30 anbi12d ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ∪ t ⊆ I ⁡ s ∪ I ⁡ t ∧ I ⁡ s ∪ I ⁡ t ⊆ I ⁡ s ∪ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∪ t → x ∈ I ⁡ s ∪ I ⁡ t ∧ ∀ x ∈ B x ∈ I ⁡ s ∪ I ⁡ t → x ∈ I ⁡ s ∪ t
32 eqss ⊢ I ⁡ s ∪ t = I ⁡ s ∪ I ⁡ t ↔ I ⁡ s ∪ t ⊆ I ⁡ s ∪ I ⁡ t ∧ I ⁡ s ∪ I ⁡ t ⊆ I ⁡ s ∪ t
33 ralbiim ⊢ ∀ x ∈ B x ∈ I ⁡ s ∪ t ↔ x ∈ I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∪ t → x ∈ I ⁡ s ∪ I ⁡ t ∧ ∀ x ∈ B x ∈ I ⁡ s ∪ I ⁡ t → x ∈ I ⁡ s ∪ t
34 31 32 33 3bitr4g ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ∪ t = I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B x ∈ I ⁡ s ∪ t ↔ x ∈ I ⁡ s ∪ I ⁡ t
35 3 ad3antrrr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → I F N
36 simpr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → x ∈ B
37 9 ad3antrrr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → B ∈ V
38 simpllr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → s ∈ 𝒫 B
39 38 elpwid ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → s ⊆ B
40 simplr ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → t ∈ 𝒫 B
41 40 elpwid ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → t ⊆ B
42 39 41 unssd ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → s ∪ t ⊆ B
43 37 42 sselpwd ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → s ∪ t ∈ 𝒫 B
44 1 2 35 36 43 ntrneiel ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ s ∪ t ↔ s ∪ t ∈ N ⁡ x
45 elun ⊢ x ∈ I ⁡ s ∪ I ⁡ t ↔ x ∈ I ⁡ s ∨ x ∈ I ⁡ t
46 1 2 35 36 38 ntrneiel ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ s ↔ s ∈ N ⁡ x
47 1 2 35 36 40 ntrneiel ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ t ↔ t ∈ N ⁡ x
48 46 47 orbi12d ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ s ∨ x ∈ I ⁡ t ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x
49 45 48 syl5bb ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ s ∪ I ⁡ t ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x
50 44 49 bibi12d ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B ∧ x ∈ B → x ∈ I ⁡ s ∪ t ↔ x ∈ I ⁡ s ∪ I ⁡ t ↔ s ∪ t ∈ N ⁡ x ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x
51 50 ralbidva ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → ∀ x ∈ B x ∈ I ⁡ s ∪ t ↔ x ∈ I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B s ∪ t ∈ N ⁡ x ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x
52 34 51 bitrd ⊢ φ ∧ s ∈ 𝒫 B ∧ t ∈ 𝒫 B → I ⁡ s ∪ t = I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B s ∪ t ∈ N ⁡ x ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x
53 52 ralbidva ⊢ φ ∧ s ∈ 𝒫 B → ∀ t ∈ 𝒫 B I ⁡ s ∪ t = I ⁡ s ∪ I ⁡ t ↔ ∀ t ∈ 𝒫 B ∀ x ∈ B s ∪ t ∈ N ⁡ x ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x
54 ralcom ⊢ ∀ t ∈ 𝒫 B ∀ x ∈ B s ∪ t ∈ N ⁡ x ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x ↔ ∀ x ∈ B ∀ t ∈ 𝒫 B s ∪ t ∈ N ⁡ x ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x
55 53 54 bitrdi ⊢ φ ∧ s ∈ 𝒫 B → ∀ t ∈ 𝒫 B I ⁡ s ∪ t = I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B ∀ t ∈ 𝒫 B s ∪ t ∈ N ⁡ x ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x
56 55 ralbidva ⊢ φ → ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∪ t = I ⁡ s ∪ I ⁡ t ↔ ∀ s ∈ 𝒫 B ∀ x ∈ B ∀ t ∈ 𝒫 B s ∪ t ∈ N ⁡ x ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x
57 ralcom ⊢ ∀ s ∈ 𝒫 B ∀ x ∈ B ∀ t ∈ 𝒫 B s ∪ t ∈ N ⁡ x ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ∪ t ∈ N ⁡ x ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x
58 56 57 bitrdi ⊢ φ → ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∪ t = I ⁡ s ∪ I ⁡ t ↔ ∀ x ∈ B ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ∪ t ∈ N ⁡ x ↔ s ∈ N ⁡ x ∨ t ∈ N ⁡ x