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 ) βˆͺ 𝐽 = βˆͺ 𝑣 )