Metamath Proof Explorer

Theorem ntrneix3

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

Ref Expression
Hypotheses ntrnei.o ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
ntrnei.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
ntrnei.r ⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
Assertion ntrneix3 ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2 ntrnei.f ⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3 ntrnei.r ⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4 dfss3 ⊢ ( ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) )
5 1 2 3 ntrneiiex ⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
6 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
7 elmapi ⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
8 6 7 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
9 1 2 3 ntrneibex ⊢ ( 𝜑 → 𝐵 ∈ V )
10 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐵 ∈ V )
11 simplr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
12 11 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑠 ⊆ 𝐵 )
13 simpr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑡 ∈ 𝒫 𝐵 )
14 13 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑡 ⊆ 𝐵 )
15 12 14 unssd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑠 ∪ 𝑡 ) ⊆ 𝐵 )
16 10 15 sselpwd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑠 ∪ 𝑡 ) ∈ 𝒫 𝐵 )
17 8 16 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ∈ 𝒫 𝐵 )
18 17 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ 𝐵 )
19 ralss ⊢ ( ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ 𝐵 → ( ∀ 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ) )
20 18 19 syl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ) )
21 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
22 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
23 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ∈ V )
24 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
25 24 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ⊆ 𝐵 )
26 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑡 ∈ 𝒫 𝐵 )
27 26 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑡 ⊆ 𝐵 )
28 25 27 unssd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑠 ∪ 𝑡 ) ⊆ 𝐵 )
29 23 28 sselpwd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑠 ∪ 𝑡 ) ∈ 𝒫 𝐵 )
30 1 2 21 22 29 ntrneiel ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ↔ ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) )
31 elun ⊢ ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) )
32 1 2 21 22 24 ntrneiel ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
33 1 2 21 22 26 ntrneiel ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ↔ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
34 32 33 orbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
35 31 34 syl5bb ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
36 30 35 imbi12d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
37 36 ralbidva ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
38 20 37 bitrd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
39 4 38 syl5bb ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
40 39 ralbidva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
41 ralcom ⊢ ( ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
42 40 41 bitrdi ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
43 42 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
44 ralcom ⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
45 43 44 bitrdi ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) → ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )