Metamath Proof Explorer


Theorem kqt0lem

Description: Lemma for kqt0 . (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis kqval.2 F = x X y J | x y
Assertion kqt0lem J TopOn X KQ J Kol2

Proof

Step Hyp Ref Expression
1 kqval.2 F = x X y J | x y
2 1 kqopn J TopOn X w J F w KQ J
3 2 adantlr J TopOn X a X b X w J F w KQ J
4 eleq2 z = F w F a z F a F w
5 eleq2 z = F w F b z F b F w
6 4 5 bibi12d z = F w F a z F b z F a F w F b F w
7 6 rspcv F w KQ J z KQ J F a z F b z F a F w F b F w
8 3 7 syl J TopOn X a X b X w J z KQ J F a z F b z F a F w F b F w
9 1 kqfvima J TopOn X w J a X a w F a F w
10 9 3expa J TopOn X w J a X a w F a F w
11 10 adantrr J TopOn X w J a X b X a w F a F w
12 1 kqfvima J TopOn X w J b X b w F b F w
13 12 3expa J TopOn X w J b X b w F b F w
14 13 adantrl J TopOn X w J a X b X b w F b F w
15 11 14 bibi12d J TopOn X w J a X b X a w b w F a F w F b F w
16 15 an32s J TopOn X a X b X w J a w b w F a F w F b F w
17 8 16 sylibrd J TopOn X a X b X w J z KQ J F a z F b z a w b w
18 17 ralrimdva J TopOn X a X b X z KQ J F a z F b z w J a w b w
19 1 kqfeq J TopOn X a X b X F a = F b y J a y b y
20 19 3expb J TopOn X a X b X F a = F b y J a y b y
21 elequ2 y = w a y a w
22 elequ2 y = w b y b w
23 21 22 bibi12d y = w a y b y a w b w
24 23 cbvralvw y J a y b y w J a w b w
25 20 24 bitrdi J TopOn X a X b X F a = F b w J a w b w
26 18 25 sylibrd J TopOn X a X b X z KQ J F a z F b z F a = F b
27 26 ralrimivva J TopOn X a X b X z KQ J F a z F b z F a = F b
28 1 kqffn J TopOn X F Fn X
29 eleq1 u = F a u z F a z
30 29 bibi1d u = F a u z v z F a z v z
31 30 ralbidv u = F a z KQ J u z v z z KQ J F a z v z
32 eqeq1 u = F a u = v F a = v
33 31 32 imbi12d u = F a z KQ J u z v z u = v z KQ J F a z v z F a = v
34 33 ralbidv u = F a v ran F z KQ J u z v z u = v v ran F z KQ J F a z v z F a = v
35 34 ralrn F Fn X u ran F v ran F z KQ J u z v z u = v a X v ran F z KQ J F a z v z F a = v
36 eleq1 v = F b v z F b z
37 36 bibi2d v = F b F a z v z F a z F b z
38 37 ralbidv v = F b z KQ J F a z v z z KQ J F a z F b z
39 eqeq2 v = F b F a = v F a = F b
40 38 39 imbi12d v = F b z KQ J F a z v z F a = v z KQ J F a z F b z F a = F b
41 40 ralrn F Fn X v ran F z KQ J F a z v z F a = v b X z KQ J F a z F b z F a = F b
42 41 ralbidv F Fn X a X v ran F z KQ J F a z v z F a = v a X b X z KQ J F a z F b z F a = F b
43 35 42 bitrd F Fn X u ran F v ran F z KQ J u z v z u = v a X b X z KQ J F a z F b z F a = F b
44 28 43 syl J TopOn X u ran F v ran F z KQ J u z v z u = v a X b X z KQ J F a z F b z F a = F b
45 27 44 mpbird J TopOn X u ran F v ran F z KQ J u z v z u = v
46 1 kqtopon J TopOn X KQ J TopOn ran F
47 ist0-2 KQ J TopOn ran F KQ J Kol2 u ran F v ran F z KQ J u z v z u = v
48 46 47 syl J TopOn X KQ J Kol2 u ran F v ran F z KQ J u z v z u = v
49 45 48 mpbird J TopOn X KQ J Kol2