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 ) ∪ 𝐽 = ∪ 𝑣 )