Metamath Proof Explorer

Theorem regr1lem

Description: Lemma for regr1 . (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypotheses kqval.2 
|- F = ( x e. X |-> { y e. J | x e. y } )
regr1lem.2 
|- ( ph -> J e. ( TopOn ` X ) )
regr1lem.3 
|- ( ph -> J e. Reg )
regr1lem.4 
|- ( ph -> A e. X )
regr1lem.5 
|- ( ph -> B e. X )
regr1lem.6 
|- ( ph -> U e. J )
regr1lem.7 
|- ( ph -> -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` A ) e. m /\ ( F ` B ) e. n /\ ( m i^i n ) = (/) ) )
Assertion regr1lem 
|- ( ph -> ( A e. U -> B e. U ) )

Proof

Step Hyp Ref Expression
1 kqval.2 
 |-  F = ( x e. X |-> { y e. J | x e. y } )
2 regr1lem.2 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 regr1lem.3 
 |-  ( ph -> J e. Reg )
4 regr1lem.4 
 |-  ( ph -> A e. X )
5 regr1lem.5 
 |-  ( ph -> B e. X )
6 regr1lem.6 
 |-  ( ph -> U e. J )
7 regr1lem.7 
 |-  ( ph -> -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` A ) e. m /\ ( F ` B ) e. n /\ ( m i^i n ) = (/) ) )
8 3 adantr 
 |-  ( ( ph /\ A e. U ) -> J e. Reg )
9 6 adantr 
 |-  ( ( ph /\ A e. U ) -> U e. J )
10 simpr 
 |-  ( ( ph /\ A e. U ) -> A e. U )
11 regsep 
 |-  ( ( J e. Reg /\ U e. J /\ A e. U ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) )
12 8 9 10 11 syl3anc 
 |-  ( ( ph /\ A e. U ) -> E. z e. J ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) )
13 7 ad2antrr 
 |-  ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) -> -. E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` A ) e. m /\ ( F ` B ) e. n /\ ( m i^i n ) = (/) ) )
14 2 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> J e. ( TopOn ` X ) )
15 simplrl 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> z e. J )
16 1 kqopn 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. J ) -> ( F " z ) e. ( KQ ` J ) )
17 14 15 16 syl2anc 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( F " z ) e. ( KQ ` J ) )
18 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
19 14 18 syl 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> X = U. J )
20 19 difeq1d 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( X \ ( ( cls ` J ) ` z ) ) = ( U. J \ ( ( cls ` J ) ` z ) ) )
21 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
22 14 21 syl 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> J e. Top )
23 elssuni 
 |-  ( z e. J -> z C_ U. J )
24 15 23 syl 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> z C_ U. J )
25 eqid 
 |-  U. J = U. J
26 25 clscld 
 |-  ( ( J e. Top /\ z C_ U. J ) -> ( ( cls ` J ) ` z ) e. ( Clsd ` J ) )
27 22 24 26 syl2anc 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( ( cls ` J ) ` z ) e. ( Clsd ` J ) )
28 25 cldopn 
 |-  ( ( ( cls ` J ) ` z ) e. ( Clsd ` J ) -> ( U. J \ ( ( cls ` J ) ` z ) ) e. J )
29 27 28 syl 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( U. J \ ( ( cls ` J ) ` z ) ) e. J )
30 20 29 eqeltrd 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( X \ ( ( cls ` J ) ` z ) ) e. J )
31 1 kqopn 
 |-  ( ( J e. ( TopOn ` X ) /\ ( X \ ( ( cls ` J ) ` z ) ) e. J ) -> ( F " ( X \ ( ( cls ` J ) ` z ) ) ) e. ( KQ ` J ) )
32 14 30 31 syl2anc 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( F " ( X \ ( ( cls ` J ) ` z ) ) ) e. ( KQ ` J ) )
33 simprrl 
 |-  ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) -> A e. z )
34 33 adantr 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> A e. z )
35 4 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> A e. X )
36 1 kqfvima 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. J /\ A e. X ) -> ( A e. z <-> ( F ` A ) e. ( F " z ) ) )
37 14 15 35 36 syl3anc 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( A e. z <-> ( F ` A ) e. ( F " z ) ) )
38 34 37 mpbid 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( F ` A ) e. ( F " z ) )
39 5 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> B e. X )
40 simprrr 
 |-  ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) -> ( ( cls ` J ) ` z ) C_ U )
41 40 sseld 
 |-  ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) -> ( B e. ( ( cls ` J ) ` z ) -> B e. U ) )
42 41 con3dimp 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> -. B e. ( ( cls ` J ) ` z ) )
43 39 42 eldifd 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> B e. ( X \ ( ( cls ` J ) ` z ) ) )
44 1 kqfvima 
 |-  ( ( J e. ( TopOn ` X ) /\ ( X \ ( ( cls ` J ) ` z ) ) e. J /\ B e. X ) -> ( B e. ( X \ ( ( cls ` J ) ` z ) ) <-> ( F ` B ) e. ( F " ( X \ ( ( cls ` J ) ` z ) ) ) ) )
45 14 30 39 44 syl3anc 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( B e. ( X \ ( ( cls ` J ) ` z ) ) <-> ( F ` B ) e. ( F " ( X \ ( ( cls ` J ) ` z ) ) ) ) )
46 43 45 mpbid 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( F ` B ) e. ( F " ( X \ ( ( cls ` J ) ` z ) ) ) )
47 25 sscls 
 |-  ( ( J e. Top /\ z C_ U. J ) -> z C_ ( ( cls ` J ) ` z ) )
48 22 24 47 syl2anc 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> z C_ ( ( cls ` J ) ` z ) )
49 48 sscond 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( X \ ( ( cls ` J ) ` z ) ) C_ ( X \ z ) )
50 imass2 
 |-  ( ( X \ ( ( cls ` J ) ` z ) ) C_ ( X \ z ) -> ( F " ( X \ ( ( cls ` J ) ` z ) ) ) C_ ( F " ( X \ z ) ) )
51 sslin 
 |-  ( ( F " ( X \ ( ( cls ` J ) ` z ) ) ) C_ ( F " ( X \ z ) ) -> ( ( F " z ) i^i ( F " ( X \ ( ( cls ` J ) ` z ) ) ) ) C_ ( ( F " z ) i^i ( F " ( X \ z ) ) ) )
52 49 50 51 3syl 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( ( F " z ) i^i ( F " ( X \ ( ( cls ` J ) ` z ) ) ) ) C_ ( ( F " z ) i^i ( F " ( X \ z ) ) ) )
53 1 kqdisj 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. J ) -> ( ( F " z ) i^i ( F " ( X \ z ) ) ) = (/) )
54 14 15 53 syl2anc 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( ( F " z ) i^i ( F " ( X \ z ) ) ) = (/) )
55 sseq0 
 |-  ( ( ( ( F " z ) i^i ( F " ( X \ ( ( cls ` J ) ` z ) ) ) ) C_ ( ( F " z ) i^i ( F " ( X \ z ) ) ) /\ ( ( F " z ) i^i ( F " ( X \ z ) ) ) = (/) ) -> ( ( F " z ) i^i ( F " ( X \ ( ( cls ` J ) ` z ) ) ) ) = (/) )
56 52 54 55 syl2anc 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> ( ( F " z ) i^i ( F " ( X \ ( ( cls ` J ) ` z ) ) ) ) = (/) )
57 eleq2 
 |-  ( m = ( F " z ) -> ( ( F ` A ) e. m <-> ( F ` A ) e. ( F " z ) ) )
58 ineq1 
 |-  ( m = ( F " z ) -> ( m i^i n ) = ( ( F " z ) i^i n ) )
59 58 eqeq1d 
 |-  ( m = ( F " z ) -> ( ( m i^i n ) = (/) <-> ( ( F " z ) i^i n ) = (/) ) )
60 57 59 3anbi13d 
 |-  ( m = ( F " z ) -> ( ( ( F ` A ) e. m /\ ( F ` B ) e. n /\ ( m i^i n ) = (/) ) <-> ( ( F ` A ) e. ( F " z ) /\ ( F ` B ) e. n /\ ( ( F " z ) i^i n ) = (/) ) ) )
61 eleq2 
 |-  ( n = ( F " ( X \ ( ( cls ` J ) ` z ) ) ) -> ( ( F ` B ) e. n <-> ( F ` B ) e. ( F " ( X \ ( ( cls ` J ) ` z ) ) ) ) )
62 ineq2 
 |-  ( n = ( F " ( X \ ( ( cls ` J ) ` z ) ) ) -> ( ( F " z ) i^i n ) = ( ( F " z ) i^i ( F " ( X \ ( ( cls ` J ) ` z ) ) ) ) )
63 62 eqeq1d 
 |-  ( n = ( F " ( X \ ( ( cls ` J ) ` z ) ) ) -> ( ( ( F " z ) i^i n ) = (/) <-> ( ( F " z ) i^i ( F " ( X \ ( ( cls ` J ) ` z ) ) ) ) = (/) ) )
64 61 63 3anbi23d 
 |-  ( n = ( F " ( X \ ( ( cls ` J ) ` z ) ) ) -> ( ( ( F ` A ) e. ( F " z ) /\ ( F ` B ) e. n /\ ( ( F " z ) i^i n ) = (/) ) <-> ( ( F ` A ) e. ( F " z ) /\ ( F ` B ) e. ( F " ( X \ ( ( cls ` J ) ` z ) ) ) /\ ( ( F " z ) i^i ( F " ( X \ ( ( cls ` J ) ` z ) ) ) ) = (/) ) ) )
65 60 64 rspc2ev 
 |-  ( ( ( F " z ) e. ( KQ ` J ) /\ ( F " ( X \ ( ( cls ` J ) ` z ) ) ) e. ( KQ ` J ) /\ ( ( F ` A ) e. ( F " z ) /\ ( F ` B ) e. ( F " ( X \ ( ( cls ` J ) ` z ) ) ) /\ ( ( F " z ) i^i ( F " ( X \ ( ( cls ` J ) ` z ) ) ) ) = (/) ) ) -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` A ) e. m /\ ( F ` B ) e. n /\ ( m i^i n ) = (/) ) )
66 17 32 38 46 56 65 syl113anc 
 |-  ( ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) /\ -. B e. U ) -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` A ) e. m /\ ( F ` B ) e. n /\ ( m i^i n ) = (/) ) )
67 66 ex 
 |-  ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) -> ( -. B e. U -> E. m e. ( KQ ` J ) E. n e. ( KQ ` J ) ( ( F ` A ) e. m /\ ( F ` B ) e. n /\ ( m i^i n ) = (/) ) ) )
68 13 67 mt3d 
 |-  ( ( ( ph /\ A e. U ) /\ ( z e. J /\ ( A e. z /\ ( ( cls ` J ) ` z ) C_ U ) ) ) -> B e. U )
69 12 68 rexlimddv 
 |-  ( ( ph /\ A e. U ) -> B e. U )
70 69 ex 
 |-  ( ph -> ( A e. U -> B e. U ) )