Metamath Proof Explorer


Theorem regr1lem

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

Ref Expression
Hypotheses kqval.2 F = x X y J | x y
regr1lem.2 φ J TopOn X
regr1lem.3 φ J Reg
regr1lem.4 φ A X
regr1lem.5 φ B X
regr1lem.6 φ U J
regr1lem.7 φ ¬ m KQ J n KQ J F A m F B n m n =
Assertion regr1lem φ A U B U

Proof

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