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 e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
ntrnei.f 
|- F = ( ~P B O B )
ntrnei.r 
|- ( ph -> I F N )
Assertion ntrneix13 
|- ( ph -> ( A. s e. ~P B A. t e. ~P B ( I ` ( s u. t ) ) = ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s u. t ) e. ( N ` x ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ntrnei.o 
 |-  O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
2 ntrnei.f 
 |-  F = ( ~P B O B )
3 ntrnei.r 
 |-  ( ph -> I F N )
4 dfss3 
 |-  ( ( I ` ( s u. t ) ) C_ ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. ( I ` ( s u. t ) ) x e. ( ( I ` s ) u. ( I ` t ) ) )
5 1 2 3 ntrneiiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
6 5 ad2antrr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> I e. ( ~P B ^m ~P B ) )
7 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
8 6 7 syl 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> I : ~P B --> ~P B )
9 1 2 3 ntrneibex 
 |-  ( ph -> B e. _V )
10 9 ad2antrr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> B e. _V )
11 simplr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> s e. ~P B )
12 11 elpwid 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> s C_ B )
13 simpr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> t e. ~P B )
14 13 elpwid 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> t C_ B )
15 12 14 unssd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( s u. t ) C_ B )
16 10 15 sselpwd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( s u. t ) e. ~P B )
17 8 16 ffvelrnd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` ( s u. t ) ) e. ~P B )
18 17 elpwid 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` ( s u. t ) ) C_ B )
19 ralss 
 |-  ( ( I ` ( s u. t ) ) C_ B -> ( A. x e. ( I ` ( s u. t ) ) x e. ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. B ( x e. ( I ` ( s u. t ) ) -> x e. ( ( I ` s ) u. ( I ` t ) ) ) ) )
20 18 19 syl 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. ( I ` ( s u. t ) ) x e. ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. B ( x e. ( I ` ( s u. t ) ) -> x e. ( ( I ` s ) u. ( I ` t ) ) ) ) )
21 4 20 syl5bb 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( I ` ( s u. t ) ) C_ ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. B ( x e. ( I ` ( s u. t ) ) -> x e. ( ( I ` s ) u. ( I ` t ) ) ) ) )
22 dfss3 
 |-  ( ( ( I ` s ) u. ( I ` t ) ) C_ ( I ` ( s u. t ) ) <-> A. x e. ( ( I ` s ) u. ( I ` t ) ) x e. ( I ` ( s u. t ) ) )
23 8 11 ffvelrnd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` s ) e. ~P B )
24 23 elpwid 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` s ) C_ B )
25 8 13 ffvelrnd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` t ) e. ~P B )
26 25 elpwid 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( I ` t ) C_ B )
27 24 26 unssd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( I ` s ) u. ( I ` t ) ) C_ B )
28 ralss 
 |-  ( ( ( I ` s ) u. ( I ` t ) ) C_ B -> ( A. x e. ( ( I ` s ) u. ( I ` t ) ) x e. ( I ` ( s u. t ) ) <-> A. x e. B ( x e. ( ( I ` s ) u. ( I ` t ) ) -> x e. ( I ` ( s u. t ) ) ) ) )
29 27 28 syl 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. ( ( I ` s ) u. ( I ` t ) ) x e. ( I ` ( s u. t ) ) <-> A. x e. B ( x e. ( ( I ` s ) u. ( I ` t ) ) -> x e. ( I ` ( s u. t ) ) ) ) )
30 22 29 syl5bb 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( ( I ` s ) u. ( I ` t ) ) C_ ( I ` ( s u. t ) ) <-> A. x e. B ( x e. ( ( I ` s ) u. ( I ` t ) ) -> x e. ( I ` ( s u. t ) ) ) ) )
31 21 30 anbi12d 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( ( I ` ( s u. t ) ) C_ ( ( I ` s ) u. ( I ` t ) ) /\ ( ( I ` s ) u. ( I ` t ) ) C_ ( I ` ( s u. t ) ) ) <-> ( A. x e. B ( x e. ( I ` ( s u. t ) ) -> x e. ( ( I ` s ) u. ( I ` t ) ) ) /\ A. x e. B ( x e. ( ( I ` s ) u. ( I ` t ) ) -> x e. ( I ` ( s u. t ) ) ) ) ) )
32 eqss 
 |-  ( ( I ` ( s u. t ) ) = ( ( I ` s ) u. ( I ` t ) ) <-> ( ( I ` ( s u. t ) ) C_ ( ( I ` s ) u. ( I ` t ) ) /\ ( ( I ` s ) u. ( I ` t ) ) C_ ( I ` ( s u. t ) ) ) )
33 ralbiim 
 |-  ( A. x e. B ( x e. ( I ` ( s u. t ) ) <-> x e. ( ( I ` s ) u. ( I ` t ) ) ) <-> ( A. x e. B ( x e. ( I ` ( s u. t ) ) -> x e. ( ( I ` s ) u. ( I ` t ) ) ) /\ A. x e. B ( x e. ( ( I ` s ) u. ( I ` t ) ) -> x e. ( I ` ( s u. t ) ) ) ) )
34 31 32 33 3bitr4g 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( I ` ( s u. t ) ) = ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. B ( x e. ( I ` ( s u. t ) ) <-> x e. ( ( I ` s ) u. ( I ` t ) ) ) ) )
35 3 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> I F N )
36 simpr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> x e. B )
37 9 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> B e. _V )
38 simpllr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> s e. ~P B )
39 38 elpwid 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> s C_ B )
40 simplr 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> t e. ~P B )
41 40 elpwid 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> t C_ B )
42 39 41 unssd 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( s u. t ) C_ B )
43 37 42 sselpwd 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( s u. t ) e. ~P B )
44 1 2 35 36 43 ntrneiel 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` ( s u. t ) ) <-> ( s u. t ) e. ( N ` x ) ) )
45 elun 
 |-  ( x e. ( ( I ` s ) u. ( I ` t ) ) <-> ( x e. ( I ` s ) \/ x e. ( I ` t ) ) )
46 1 2 35 36 38 ntrneiel 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` s ) <-> s e. ( N ` x ) ) )
47 1 2 35 36 40 ntrneiel 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( I ` t ) <-> t e. ( N ` x ) ) )
48 46 47 orbi12d 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( x e. ( I ` s ) \/ x e. ( I ` t ) ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) )
49 45 48 syl5bb 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( x e. ( ( I ` s ) u. ( I ` t ) ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) )
50 44 49 bibi12d 
 |-  ( ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) /\ x e. B ) -> ( ( x e. ( I ` ( s u. t ) ) <-> x e. ( ( I ` s ) u. ( I ` t ) ) ) <-> ( ( s u. t ) e. ( N ` x ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )
51 50 ralbidva 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( A. x e. B ( x e. ( I ` ( s u. t ) ) <-> x e. ( ( I ` s ) u. ( I ` t ) ) ) <-> A. x e. B ( ( s u. t ) e. ( N ` x ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )
52 34 51 bitrd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( ( I ` ( s u. t ) ) = ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. B ( ( s u. t ) e. ( N ` x ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )
53 52 ralbidva 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( I ` ( s u. t ) ) = ( ( I ` s ) u. ( I ` t ) ) <-> A. t e. ~P B A. x e. B ( ( s u. t ) e. ( N ` x ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )
54 ralcom 
 |-  ( A. t e. ~P B A. x e. B ( ( s u. t ) e. ( N ` x ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) <-> A. x e. B A. t e. ~P B ( ( s u. t ) e. ( N ` x ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) )
55 53 54 bitrdi 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. t e. ~P B ( I ` ( s u. t ) ) = ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. B A. t e. ~P B ( ( s u. t ) e. ( N ` x ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )
56 55 ralbidva 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( I ` ( s u. t ) ) = ( ( I ` s ) u. ( I ` t ) ) <-> A. s e. ~P B A. x e. B A. t e. ~P B ( ( s u. t ) e. ( N ` x ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )
57 ralcom 
 |-  ( A. s e. ~P B A. x e. B A. t e. ~P B ( ( s u. t ) e. ( N ` x ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s u. t ) e. ( N ` x ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) )
58 56 57 bitrdi 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( I ` ( s u. t ) ) = ( ( I ` s ) u. ( I ` t ) ) <-> A. x e. B A. s e. ~P B A. t e. ~P B ( ( s u. t ) e. ( N ` x ) <-> ( s e. ( N ` x ) \/ t e. ( N ` x ) ) ) ) )