# Metamath Proof Explorer

## Theorem kqt0lem

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

Ref Expression
Hypothesis kqval.2 ${⊢}{F}=\left({x}\in {X}⟼\left\{{y}\in {J}|{x}\in {y}\right\}\right)$
Assertion kqt0lem ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to \mathrm{KQ}\left({J}\right)\in \mathrm{Kol2}$

### Proof

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