Theorem heiborlem2

Description: Lemma for heibor . Substitutions for the set G . (Contributed by Jeff Madsen, 23-Jan-2014)

	Ref	Expression
Hypotheses	heibor.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	heibor.3	⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
	heibor.4	⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
	heiborlem2.5	⊢ 𝐴 ∈ V
	heiborlem2.6	⊢ 𝐶 ∈ V
Assertion	heiborlem2	⊢ ( 𝐴 𝐺 𝐶 ↔ ( 𝐶 ∈ ℕ0 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐴 𝐵 𝐶 ) ∈ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		heibor.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		heibor.3	⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
3		heibor.4	⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
4		heiborlem2.5	⊢ 𝐴 ∈ V
5		heiborlem2.6	⊢ 𝐶 ∈ V
6		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ↔ 𝐴 ∈ ( 𝐹 ‘ 𝑛 ) ) )
7		oveq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 𝐵 𝑛 ) = ( 𝐴 𝐵 𝑛 ) )
8	7	eleq1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ↔ ( 𝐴 𝐵 𝑛 ) ∈ 𝐾 ) )
9	6 8	3anbi23d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑛 ∈ ℕ0 ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) ↔ ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝐴 𝐵 𝑛 ) ∈ 𝐾 ) ) )
10		eleq1	⊢ ( 𝑛 = 𝐶 → ( 𝑛 ∈ ℕ0 ↔ 𝐶 ∈ ℕ0 ) )
11		fveq2	⊢ ( 𝑛 = 𝐶 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝐶 ) )
12	11	eleq2d	⊢ ( 𝑛 = 𝐶 → ( 𝐴 ∈ ( 𝐹 ‘ 𝑛 ) ↔ 𝐴 ∈ ( 𝐹 ‘ 𝐶 ) ) )
13		oveq2	⊢ ( 𝑛 = 𝐶 → ( 𝐴 𝐵 𝑛 ) = ( 𝐴 𝐵 𝐶 ) )
14	13	eleq1d	⊢ ( 𝑛 = 𝐶 → ( ( 𝐴 𝐵 𝑛 ) ∈ 𝐾 ↔ ( 𝐴 𝐵 𝐶 ) ∈ 𝐾 ) )
15	10 12 14	3anbi123d	⊢ ( 𝑛 = 𝐶 → ( ( 𝑛 ∈ ℕ0 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝐴 𝐵 𝑛 ) ∈ 𝐾 ) ↔ ( 𝐶 ∈ ℕ0 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐴 𝐵 𝐶 ) ∈ 𝐾 ) ) )
16	4 5 9 15 3	brab	⊢ ( 𝐴 𝐺 𝐶 ↔ ( 𝐶 ∈ ℕ0 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐴 𝐵 𝐶 ) ∈ 𝐾 ) )