Metamath Proof Explorer

Theorem heiborlem10

Description: Lemma for heibor . The last remaining piece of the proof is to find an element C such that C G 0 , i.e. C is an element of ( F0 ) that has no finite subcover, which is true by heiborlem1 , since ( F0 ) is a finite cover of X , which has no finite subcover. Thus, the rest of the proof follows to a contradiction, and thus there must be a finite subcover of U that covers X , i.e. X is compact. (Contributed by Jeff Madsen, 22-Jan-2014)

Ref Expression
Hypotheses heibor.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
heibor.3 ⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
heibor.4 ⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
heibor.5 ⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
heibor.6 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
heibor.7 ⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
heibor.8 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
Assertion heiborlem10 ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∪ 𝐽 = ∪ 𝑣 )

Proof

Step Hyp Ref Expression
1 heibor.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 heibor.3 ⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
3 heibor.4 ⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
4 heibor.5 ⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ0 ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
5 heibor.6 ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
6 heibor.7 ⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
7 heibor.8 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
8 0nn0 ⊢ 0 ∈ ℕ0
9 inss2 ⊢ ( 𝒫 𝑋 ∩ Fin ) ⊆ Fin
10 ffvelcdm ⊢ ( ( 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) ∧ 0 ∈ ℕ0 ) → ( 𝐹 ‘ 0 ) ∈ ( 𝒫 𝑋 ∩ Fin ) )
11 9 10 sselid ⊢ ( ( 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) ∧ 0 ∈ ℕ0 ) → ( 𝐹 ‘ 0 ) ∈ Fin )
12 6 8 11 sylancl ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) ∈ Fin )
13 fveq2 ⊢ ( 𝑛 = 0 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 0 ) )
14 oveq2 ⊢ ( 𝑛 = 0 → ( 𝑦 𝐵 𝑛 ) = ( 𝑦 𝐵 0 ) )
15 13 14 iuneq12d ⊢ ( 𝑛 = 0 → ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 0 ) ( 𝑦 𝐵 0 ) )
16 15 eqeq2d ⊢ ( 𝑛 = 0 → ( 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) ↔ 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 0 ) ( 𝑦 𝐵 0 ) ) )
17 16 rspccva ⊢ ( ( ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) ∧ 0 ∈ ℕ0 ) → 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 0 ) ( 𝑦 𝐵 0 ) )
18 7 8 17 sylancl ⊢ ( 𝜑 → 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 0 ) ( 𝑦 𝐵 0 ) )
19 eqimss ⊢ ( 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 0 ) ( 𝑦 𝐵 0 ) → 𝑋 ⊆ ∪ 𝑦 ∈ ( 𝐹 ‘ 0 ) ( 𝑦 𝐵 0 ) )
20 18 19 syl ⊢ ( 𝜑 → 𝑋 ⊆ ∪ 𝑦 ∈ ( 𝐹 ‘ 0 ) ( 𝑦 𝐵 0 ) )
21 ovex ⊢ ( 𝑦 𝐵 0 ) ∈ V
22 1 2 21 heiborlem1 ⊢ ( ( ( 𝐹 ‘ 0 ) ∈ Fin ∧ 𝑋 ⊆ ∪ 𝑦 ∈ ( 𝐹 ‘ 0 ) ( 𝑦 𝐵 0 ) ∧ 𝑋 ∈ 𝐾 ) → ∃ 𝑦 ∈ ( 𝐹 ‘ 0 ) ( 𝑦 𝐵 0 ) ∈ 𝐾 )
23 oveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 𝐵 0 ) = ( 𝑥 𝐵 0 ) )
24 23 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 𝐵 0 ) ∈ 𝐾 ↔ ( 𝑥 𝐵 0 ) ∈ 𝐾 ) )
25 24 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ( 𝐹 ‘ 0 ) ( 𝑦 𝐵 0 ) ∈ 𝐾 ↔ ∃ 𝑥 ∈ ( 𝐹 ‘ 0 ) ( 𝑥 𝐵 0 ) ∈ 𝐾 )
26 22 25 sylib ⊢ ( ( ( 𝐹 ‘ 0 ) ∈ Fin ∧ 𝑋 ⊆ ∪ 𝑦 ∈ ( 𝐹 ‘ 0 ) ( 𝑦 𝐵 0 ) ∧ 𝑋 ∈ 𝐾 ) → ∃ 𝑥 ∈ ( 𝐹 ‘ 0 ) ( 𝑥 𝐵 0 ) ∈ 𝐾 )
27 26 3expia ⊢ ( ( ( 𝐹 ‘ 0 ) ∈ Fin ∧ 𝑋 ⊆ ∪ 𝑦 ∈ ( 𝐹 ‘ 0 ) ( 𝑦 𝐵 0 ) ) → ( 𝑋 ∈ 𝐾 → ∃ 𝑥 ∈ ( 𝐹 ‘ 0 ) ( 𝑥 𝐵 0 ) ∈ 𝐾 ) )
28 12 20 27 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐾 → ∃ 𝑥 ∈ ( 𝐹 ‘ 0 ) ( 𝑥 𝐵 0 ) ∈ 𝐾 ) )
29 28 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ( 𝑋 ∈ 𝐾 → ∃ 𝑥 ∈ ( 𝐹 ‘ 0 ) ( 𝑥 𝐵 0 ) ∈ 𝐾 ) )
30 vex ⊢ 𝑥 ∈ V
31 c0ex ⊢ 0 ∈ V
32 1 2 3 30 31 heiborlem2 ⊢ ( 𝑥 𝐺 0 ↔ ( 0 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝐹 ‘ 0 ) ∧ ( 𝑥 𝐵 0 ) ∈ 𝐾 ) )
33 1 2 3 4 5 6 7 heiborlem3 ⊢ ( 𝜑 → ∃ 𝑔 ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
34 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ 𝑥 𝐺 0 ) → ∃ 𝑔 ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
35 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ ( 𝑥 𝐺 0 ∧ ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
36 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ ( 𝑥 𝐺 0 ∧ ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) ) → 𝐹 : ℕ0 ⟶ ( 𝒫 𝑋 ∩ Fin ) )
37 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ ( 𝑥 𝐺 0 ∧ ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) ) → ∀ 𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
38 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ ( 𝑥 𝐺 0 ∧ ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) ) → ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
39 fveq2 ⊢ ( 𝑥 = 𝑡 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑡 ) )
40 fveq2 ⊢ ( 𝑥 = 𝑡 → ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑡 ) )
41 40 oveq1d ⊢ ( 𝑥 = 𝑡 → ( ( 2nd ‘ 𝑥 ) + 1 ) = ( ( 2nd ‘ 𝑡 ) + 1 ) )
42 39 41 breq12d ⊢ ( 𝑥 = 𝑡 → ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ↔ ( 𝑔 ‘ 𝑡 ) 𝐺 ( ( 2nd ‘ 𝑡 ) + 1 ) ) )
43 fveq2 ⊢ ( 𝑥 = 𝑡 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑡 ) )
44 39 41 oveq12d ⊢ ( 𝑥 = 𝑡 → ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) = ( ( 𝑔 ‘ 𝑡 ) 𝐵 ( ( 2nd ‘ 𝑡 ) + 1 ) ) )
45 43 44 ineq12d ⊢ ( 𝑥 = 𝑡 → ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) = ( ( 𝐵 ‘ 𝑡 ) ∩ ( ( 𝑔 ‘ 𝑡 ) 𝐵 ( ( 2nd ‘ 𝑡 ) + 1 ) ) ) )
46 45 eleq1d ⊢ ( 𝑥 = 𝑡 → ( ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ↔ ( ( 𝐵 ‘ 𝑡 ) ∩ ( ( 𝑔 ‘ 𝑡 ) 𝐵 ( ( 2nd ‘ 𝑡 ) + 1 ) ) ) ∈ 𝐾 ) )
47 42 46 anbi12d ⊢ ( 𝑥 = 𝑡 → ( ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ↔ ( ( 𝑔 ‘ 𝑡 ) 𝐺 ( ( 2nd ‘ 𝑡 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑡 ) ∩ ( ( 𝑔 ‘ 𝑡 ) 𝐵 ( ( 2nd ‘ 𝑡 ) + 1 ) ) ) ∈ 𝐾 ) ) )
48 47 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ↔ ∀ 𝑡 ∈ 𝐺 ( ( 𝑔 ‘ 𝑡 ) 𝐺 ( ( 2nd ‘ 𝑡 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑡 ) ∩ ( ( 𝑔 ‘ 𝑡 ) 𝐵 ( ( 2nd ‘ 𝑡 ) + 1 ) ) ) ∈ 𝐾 ) )
49 38 48 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ ( 𝑥 𝐺 0 ∧ ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) ) → ∀ 𝑡 ∈ 𝐺 ( ( 𝑔 ‘ 𝑡 ) 𝐺 ( ( 2nd ‘ 𝑡 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑡 ) ∩ ( ( 𝑔 ‘ 𝑡 ) 𝐵 ( ( 2nd ‘ 𝑡 ) + 1 ) ) ) ∈ 𝐾 ) )
50 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ ( 𝑥 𝐺 0 ∧ ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) ) → 𝑥 𝐺 0 )
51 eqeq1 ⊢ ( 𝑔 = 𝑚 → ( 𝑔 = 0 ↔ 𝑚 = 0 ) )
52 oveq1 ⊢ ( 𝑔 = 𝑚 → ( 𝑔 − 1 ) = ( 𝑚 − 1 ) )
53 51 52 ifbieq2d ⊢ ( 𝑔 = 𝑚 → if ( 𝑔 = 0 , 𝑥 , ( 𝑔 − 1 ) ) = if ( 𝑚 = 0 , 𝑥 , ( 𝑚 − 1 ) ) )
54 53 cbvmptv ⊢ ( 𝑔 ∈ ℕ0 ↦ if ( 𝑔 = 0 , 𝑥 , ( 𝑔 − 1 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝑥 , ( 𝑚 − 1 ) ) )
55 seqeq3 ⊢ ( ( 𝑔 ∈ ℕ0 ↦ if ( 𝑔 = 0 , 𝑥 , ( 𝑔 − 1 ) ) ) = ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝑥 , ( 𝑚 − 1 ) ) ) → seq 0 ( 𝑔 , ( 𝑔 ∈ ℕ0 ↦ if ( 𝑔 = 0 , 𝑥 , ( 𝑔 − 1 ) ) ) ) = seq 0 ( 𝑔 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝑥 , ( 𝑚 − 1 ) ) ) ) )
56 54 55 ax-mp ⊢ seq 0 ( 𝑔 , ( 𝑔 ∈ ℕ0 ↦ if ( 𝑔 = 0 , 𝑥 , ( 𝑔 − 1 ) ) ) ) = seq 0 ( 𝑔 , ( 𝑚 ∈ ℕ0 ↦ if ( 𝑚 = 0 , 𝑥 , ( 𝑚 − 1 ) ) ) )
57 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ⟨ ( seq 0 ( 𝑔 , ( 𝑔 ∈ ℕ0 ↦ if ( 𝑔 = 0 , 𝑥 , ( 𝑔 − 1 ) ) ) ) ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ ) = ( 𝑛 ∈ ℕ ↦ ⟨ ( seq 0 ( 𝑔 , ( 𝑔 ∈ ℕ0 ↦ if ( 𝑔 = 0 , 𝑥 , ( 𝑔 − 1 ) ) ) ) ‘ 𝑛 ) , ( 3 / ( 2 ↑ 𝑛 ) ) ⟩ )
58 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ ( 𝑥 𝐺 0 ∧ ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) ) → 𝑈 ⊆ 𝐽 )
59 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
60 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
61 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
62 5 59 60 61 4syl ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
63 62 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → 𝑋 = ∪ 𝐽 )
64 simprr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ∪ 𝐽 = ∪ 𝑈 )
65 63 64 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ∪ 𝑈 = 𝑋 )
66 65 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ ( 𝑥 𝐺 0 ∧ ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) ) → ∪ 𝑈 = 𝑋 )
67 1 2 3 4 35 36 37 49 50 56 57 58 66 heiborlem9 ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ ( 𝑥 𝐺 0 ∧ ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) ) → ¬ 𝑋 ∈ 𝐾 )
68 67 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ 𝑥 𝐺 0 ) → ( ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) → ¬ 𝑋 ∈ 𝐾 ) )
69 68 exlimdv ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ 𝑥 𝐺 0 ) → ( ∃ 𝑔 ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) → ¬ 𝑋 ∈ 𝐾 ) )
70 34 69 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ 𝑥 𝐺 0 ) → ¬ 𝑋 ∈ 𝐾 )
71 32 70 sylan2br ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ ( 0 ∈ ℕ0 ∧ 𝑥 ∈ ( 𝐹 ‘ 0 ) ∧ ( 𝑥 𝐵 0 ) ∈ 𝐾 ) ) → ¬ 𝑋 ∈ 𝐾 )
72 71 3exp2 ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ( 0 ∈ ℕ0 → ( 𝑥 ∈ ( 𝐹 ‘ 0 ) → ( ( 𝑥 𝐵 0 ) ∈ 𝐾 → ¬ 𝑋 ∈ 𝐾 ) ) ) )
73 8 72 mpi ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ( 𝑥 ∈ ( 𝐹 ‘ 0 ) → ( ( 𝑥 𝐵 0 ) ∈ 𝐾 → ¬ 𝑋 ∈ 𝐾 ) ) )
74 73 rexlimdv ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ( ∃ 𝑥 ∈ ( 𝐹 ‘ 0 ) ( 𝑥 𝐵 0 ) ∈ 𝐾 → ¬ 𝑋 ∈ 𝐾 ) )
75 29 74 syld ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ( 𝑋 ∈ 𝐾 → ¬ 𝑋 ∈ 𝐾 ) )
76 75 pm2.01d ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ¬ 𝑋 ∈ 𝐾 )
77 elfvdm ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝑋 ∈ dom CMet )
78 sseq1 ⊢ ( 𝑢 = 𝑋 → ( 𝑢 ⊆ ∪ 𝑣 ↔ 𝑋 ⊆ ∪ 𝑣 ) )
79 78 rexbidv ⊢ ( 𝑢 = 𝑋 → ( ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 ↔ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 ⊆ ∪ 𝑣 ) )
80 79 notbid ⊢ ( 𝑢 = 𝑋 → ( ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 ⊆ ∪ 𝑣 ) )
81 80 2 elab2g ⊢ ( 𝑋 ∈ dom CMet → ( 𝑋 ∈ 𝐾 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 ⊆ ∪ 𝑣 ) )
82 5 77 81 3syl ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐾 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 ⊆ ∪ 𝑣 ) )
83 82 adantr ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ( 𝑋 ∈ 𝐾 ↔ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 ⊆ ∪ 𝑣 ) )
84 83 con2bid ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 ⊆ ∪ 𝑣 ↔ ¬ 𝑋 ∈ 𝐾 ) )
85 76 84 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 ⊆ ∪ 𝑣 )
86 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → 𝑋 = ∪ 𝐽 )
87 86 sseq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑋 ⊆ ∪ 𝑣 ↔ ∪ 𝐽 ⊆ ∪ 𝑣 ) )
88 inss1 ⊢ ( 𝒫 𝑈 ∩ Fin ) ⊆ 𝒫 𝑈
89 88 sseli ⊢ ( 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑣 ∈ 𝒫 𝑈 )
90 89 elpwid ⊢ ( 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) → 𝑣 ⊆ 𝑈 )
91 simprl ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → 𝑈 ⊆ 𝐽 )
92 sstr ⊢ ( ( 𝑣 ⊆ 𝑈 ∧ 𝑈 ⊆ 𝐽 ) → 𝑣 ⊆ 𝐽 )
93 92 unissd ⊢ ( ( 𝑣 ⊆ 𝑈 ∧ 𝑈 ⊆ 𝐽 ) → ∪ 𝑣 ⊆ ∪ 𝐽 )
94 90 91 93 syl2anr ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ∪ 𝑣 ⊆ ∪ 𝐽 )
95 94 biantrud ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( ∪ 𝐽 ⊆ ∪ 𝑣 ↔ ( ∪ 𝐽 ⊆ ∪ 𝑣 ∧ ∪ 𝑣 ⊆ ∪ 𝐽 ) ) )
96 eqss ⊢ ( ∪ 𝐽 = ∪ 𝑣 ↔ ( ∪ 𝐽 ⊆ ∪ 𝑣 ∧ ∪ 𝑣 ⊆ ∪ 𝐽 ) )
97 95 96 bitr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( ∪ 𝐽 ⊆ ∪ 𝑣 ↔ ∪ 𝐽 = ∪ 𝑣 ) )
98 87 97 bitrd ⊢ ( ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) ∧ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ) → ( 𝑋 ⊆ ∪ 𝑣 ↔ ∪ 𝐽 = ∪ 𝑣 ) )
99 98 rexbidva ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 ⊆ ∪ 𝑣 ↔ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∪ 𝐽 = ∪ 𝑣 ) )
100 85 99 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪ 𝑈 ) ) → ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) ∪ 𝐽 = ∪ 𝑣 )