Metamath Proof Explorer

Theorem kqt0lem

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

Ref Expression
Hypothesis kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
Assertion kqt0lem ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ Kol2 )

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2 1 kqopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ) → ( 𝐹 “ 𝑤 ) ∈ ( KQ ‘ 𝐽 ) )
3 2 adantlr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ 𝑤 ∈ 𝐽 ) → ( 𝐹 “ 𝑤 ) ∈ ( KQ ‘ 𝐽 ) )
4 eleq2 ⊢ ( 𝑧 = ( 𝐹 “ 𝑤 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝑤 ) ) )
5 eleq2 ⊢ ( 𝑧 = ( 𝐹 “ 𝑤 ) → ( ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝑤 ) ) )
6 4 5 bibi12d ⊢ ( 𝑧 = ( 𝐹 “ 𝑤 ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝑤 ) ↔ ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝑤 ) ) ) )
7 6 rspcv ⊢ ( ( 𝐹 “ 𝑤 ) ∈ ( KQ ‘ 𝐽 ) → ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝑤 ) ↔ ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝑤 ) ) ) )
8 3 7 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ 𝑤 ∈ 𝐽 ) → ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝑤 ) ↔ ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝑤 ) ) ) )
9 1 kqfvima ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ∧ 𝑎 ∈ 𝑋 ) → ( 𝑎 ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝑤 ) ) )
10 9 3expa ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ) ∧ 𝑎 ∈ 𝑋 ) → ( 𝑎 ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝑤 ) ) )
11 10 adantrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑎 ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝑤 ) ) )
12 1 kqfvima ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ∧ 𝑏 ∈ 𝑋 ) → ( 𝑏 ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝑤 ) ) )
13 12 3expa ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ) ∧ 𝑏 ∈ 𝑋 ) → ( 𝑏 ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝑤 ) ) )
14 13 adantrl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( 𝑏 ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝑤 ) ) )
15 11 14 bibi12d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝑎 ∈ 𝑤 ↔ 𝑏 ∈ 𝑤 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝑤 ) ↔ ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝑤 ) ) ) )
16 15 an32s ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ 𝑤 ∈ 𝐽 ) → ( ( 𝑎 ∈ 𝑤 ↔ 𝑏 ∈ 𝑤 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝑤 ) ↔ ( 𝐹 ‘ 𝑏 ) ∈ ( 𝐹 “ 𝑤 ) ) ) )
17 8 16 sylibrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) ∧ 𝑤 ∈ 𝐽 ) → ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) → ( 𝑎 ∈ 𝑤 ↔ 𝑏 ∈ 𝑤 ) ) )
18 17 ralrimdva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) → ∀ 𝑤 ∈ 𝐽 ( 𝑎 ∈ 𝑤 ↔ 𝑏 ∈ 𝑤 ) ) )
19 1 kqfeq ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑎 ∈ 𝑦 ↔ 𝑏 ∈ 𝑦 ) ) )
20 19 3expb ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ↔ ∀ 𝑦 ∈ 𝐽 ( 𝑎 ∈ 𝑦 ↔ 𝑏 ∈ 𝑦 ) ) )
21 elequ2 ⊢ ( 𝑦 = 𝑤 → ( 𝑎 ∈ 𝑦 ↔ 𝑎 ∈ 𝑤 ) )
22 elequ2 ⊢ ( 𝑦 = 𝑤 → ( 𝑏 ∈ 𝑦 ↔ 𝑏 ∈ 𝑤 ) )
23 21 22 bibi12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑎 ∈ 𝑦 ↔ 𝑏 ∈ 𝑦 ) ↔ ( 𝑎 ∈ 𝑤 ↔ 𝑏 ∈ 𝑤 ) ) )
24 23 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝐽 ( 𝑎 ∈ 𝑦 ↔ 𝑏 ∈ 𝑦 ) ↔ ∀ 𝑤 ∈ 𝐽 ( 𝑎 ∈ 𝑤 ↔ 𝑏 ∈ 𝑤 ) )
25 20 24 bitrdi ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ↔ ∀ 𝑤 ∈ 𝐽 ( 𝑎 ∈ 𝑤 ↔ 𝑏 ∈ 𝑤 ) ) )
26 18 25 sylibrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ) ) → ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) )
27 26 ralrimivva ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) )
28 1 kqffn ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
29 eleq1 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑎 ) → ( 𝑢 ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ) )
30 29 bibi1d ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑎 ) → ( ( 𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) ) )
31 30 ralbidv ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑎 ) → ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( 𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) ) )
32 eqeq1 ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑎 ) → ( 𝑢 = 𝑣 ↔ ( 𝐹 ‘ 𝑎 ) = 𝑣 ) )
33 31 32 imbi12d ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑎 ) → ( ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( 𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → 𝑢 = 𝑣 ) ↔ ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = 𝑣 ) ) )
34 33 ralbidv ⊢ ( 𝑢 = ( 𝐹 ‘ 𝑎 ) → ( ∀ 𝑣 ∈ ran 𝐹 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( 𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑣 ∈ ran 𝐹 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = 𝑣 ) ) )
35 34 ralrn ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑢 ∈ ran 𝐹 ∀ 𝑣 ∈ ran 𝐹 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( 𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑣 ∈ ran 𝐹 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = 𝑣 ) ) )
36 eleq1 ⊢ ( 𝑣 = ( 𝐹 ‘ 𝑏 ) → ( 𝑣 ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) )
37 36 bibi2d ⊢ ( 𝑣 = ( 𝐹 ‘ 𝑏 ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) ) )
38 37 ralbidv ⊢ ( 𝑣 = ( 𝐹 ‘ 𝑏 ) → ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) ↔ ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) ) )
39 eqeq2 ⊢ ( 𝑣 = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ 𝑎 ) = 𝑣 ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) )
40 38 39 imbi12d ⊢ ( 𝑣 = ( 𝐹 ‘ 𝑏 ) → ( ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = 𝑣 ) ↔ ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ) )
41 40 ralrn ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑣 ∈ ran 𝐹 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = 𝑣 ) ↔ ∀ 𝑏 ∈ 𝑋 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ) )
42 41 ralbidv ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑎 ∈ 𝑋 ∀ 𝑣 ∈ ran 𝐹 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = 𝑣 ) ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ) )
43 35 42 bitrd ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑢 ∈ ran 𝐹 ∀ 𝑣 ∈ ran 𝐹 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( 𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ) )
44 28 43 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑢 ∈ ran 𝐹 ∀ 𝑣 ∈ ran 𝐹 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( 𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑋 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑧 ↔ ( 𝐹 ‘ 𝑏 ) ∈ 𝑧 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ) )
45 27 44 mpbird ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∀ 𝑢 ∈ ran 𝐹 ∀ 𝑣 ∈ ran 𝐹 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( 𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → 𝑢 = 𝑣 ) )
46 1 kqtopon ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) )
47 ist0-2 ⊢ ( ( KQ ‘ 𝐽 ) ∈ ( TopOn ‘ ran 𝐹 ) → ( ( KQ ‘ 𝐽 ) ∈ Kol2 ↔ ∀ 𝑢 ∈ ran 𝐹 ∀ 𝑣 ∈ ran 𝐹 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( 𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → 𝑢 = 𝑣 ) ) )
48 46 47 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( KQ ‘ 𝐽 ) ∈ Kol2 ↔ ∀ 𝑢 ∈ ran 𝐹 ∀ 𝑣 ∈ ran 𝐹 ( ∀ 𝑧 ∈ ( KQ ‘ 𝐽 ) ( 𝑢 ∈ 𝑧 ↔ 𝑣 ∈ 𝑧 ) → 𝑢 = 𝑣 ) ) )
49 45 48 mpbird ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) ∈ Kol2 )