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