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∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
ntrnei.f ⊢F=𝒫BOB
ntrnei.r ⊢φ→IFN
Assertion ntrneix13 ⊢φ→∀s∈𝒫B∀t∈𝒫BI⁡s∪t=I⁡s∪I⁡t↔∀x∈B∀s∈𝒫B∀t∈𝒫Bs∪t∈N⁡x↔s∈N⁡x∨t∈N⁡x

Proof

Step Hyp Ref Expression
1 ntrnei.o ⊢O=i∈V,j∈V⟼k∈𝒫ji⟼l∈j⟼m∈i|l∈k⁡m
2 ntrnei.f ⊢F=𝒫BOB
3 ntrnei.r ⊢φ→IFN
4 dfss3 ⊢I⁡s∪t⊆I⁡s∪I⁡t↔∀x∈I⁡s∪tx∈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 ffvelcdmd ⊢φ∧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∪tx∈I⁡s∪I⁡t↔∀x∈Bx∈I⁡s∪t→x∈I⁡s∪I⁡t
20 18 19 syl ⊢φ∧s∈𝒫B∧t∈𝒫B→∀x∈I⁡s∪tx∈I⁡s∪I⁡t↔∀x∈Bx∈I⁡s∪t→x∈I⁡s∪I⁡t
21 4 20 bitrid ⊢φ∧s∈𝒫B∧t∈𝒫B→I⁡s∪t⊆I⁡s∪I⁡t↔∀x∈Bx∈I⁡s∪t→x∈I⁡s∪I⁡t
22 dfss3 ⊢I⁡s∪I⁡t⊆I⁡s∪t↔∀x∈I⁡s∪I⁡tx∈I⁡s∪t
23 8 11 ffvelcdmd ⊢φ∧s∈𝒫B∧t∈𝒫B→I⁡s∈𝒫B
24 23 elpwid ⊢φ∧s∈𝒫B∧t∈𝒫B→I⁡s⊆B
25 8 13 ffvelcdmd ⊢φ∧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⁡tx∈I⁡s∪t↔∀x∈Bx∈I⁡s∪I⁡t→x∈I⁡s∪t
29 27 28 syl ⊢φ∧s∈𝒫B∧t∈𝒫B→∀x∈I⁡s∪I⁡tx∈I⁡s∪t↔∀x∈Bx∈I⁡s∪I⁡t→x∈I⁡s∪t
30 22 29 bitrid ⊢φ∧s∈𝒫B∧t∈𝒫B→I⁡s∪I⁡t⊆I⁡s∪t↔∀x∈Bx∈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∈Bx∈I⁡s∪t→x∈I⁡s∪I⁡t∧∀x∈Bx∈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∈Bx∈I⁡s∪t↔x∈I⁡s∪I⁡t↔∀x∈Bx∈I⁡s∪t→x∈I⁡s∪I⁡t∧∀x∈Bx∈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∈Bx∈I⁡s∪t↔x∈I⁡s∪I⁡t
35 3 ad3antrrr ⊢φ∧s∈𝒫B∧t∈𝒫B∧x∈B→IFN
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 bitrid ⊢φ∧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∈Bx∈I⁡s∪t↔x∈I⁡s∪I⁡t↔∀x∈Bs∪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∈Bs∪t∈N⁡x↔s∈N⁡x∨t∈N⁡x
53 52 ralbidva ⊢φ∧s∈𝒫B→∀t∈𝒫BI⁡s∪t=I⁡s∪I⁡t↔∀t∈𝒫B∀x∈Bs∪t∈N⁡x↔s∈N⁡x∨t∈N⁡x
54 ralcom ⊢∀t∈𝒫B∀x∈Bs∪t∈N⁡x↔s∈N⁡x∨t∈N⁡x↔∀x∈B∀t∈𝒫Bs∪t∈N⁡x↔s∈N⁡x∨t∈N⁡x
55 53 54 bitrdi ⊢φ∧s∈𝒫B→∀t∈𝒫BI⁡s∪t=I⁡s∪I⁡t↔∀x∈B∀t∈𝒫Bs∪t∈N⁡x↔s∈N⁡x∨t∈N⁡x
56 55 ralbidva ⊢φ→∀s∈𝒫B∀t∈𝒫BI⁡s∪t=I⁡s∪I⁡t↔∀s∈𝒫B∀x∈B∀t∈𝒫Bs∪t∈N⁡x↔s∈N⁡x∨t∈N⁡x
57 ralcom ⊢∀s∈𝒫B∀x∈B∀t∈𝒫Bs∪t∈N⁡x↔s∈N⁡x∨t∈N⁡x↔∀x∈B∀s∈𝒫B∀t∈𝒫Bs∪t∈N⁡x↔s∈N⁡x∨t∈N⁡x
58 56 57 bitrdi ⊢φ→∀s∈𝒫B∀t∈𝒫BI⁡s∪t=I⁡s∪I⁡t↔∀x∈B∀s∈𝒫B∀t∈𝒫Bs∪t∈N⁡x↔s∈N⁡x∨t∈N⁡x