Metamath Proof Explorer

Theorem heiborlem2

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

Ref Expression
Hypotheses heibor.1 ⊢J=MetOpen⁡D
heibor.3 ⊢K=u|¬∃v∈𝒫U∩Finu⊆⋃v
heibor.4 ⊢G=yn|n∈ℕ0∧y∈F⁡n∧yBn∈K
heiborlem2.5 ⊢A∈V
heiborlem2.6 ⊢C∈V
Assertion heiborlem2 ⊢AGC↔C∈ℕ0∧A∈F⁡C∧ABC∈K

Proof

Step Hyp Ref Expression
1 heibor.1 ⊢J=MetOpen⁡D
2 heibor.3 ⊢K=u|¬∃v∈𝒫U∩Finu⊆⋃v
3 heibor.4 ⊢G=yn|n∈ℕ0∧y∈F⁡n∧yBn∈K
4 heiborlem2.5 ⊢A∈V
5 heiborlem2.6 ⊢C∈V
6 eleq1 ⊢y=A→y∈F⁡n↔A∈F⁡n
7 oveq1 ⊢y=A→yBn=ABn
8 7 eleq1d ⊢y=A→yBn∈K↔ABn∈K
9 6 8 3anbi23d ⊢y=A→n∈ℕ0∧y∈F⁡n∧yBn∈K↔n∈ℕ0∧A∈F⁡n∧ABn∈K
10 eleq1 ⊢n=C→n∈ℕ0↔C∈ℕ0
11 fveq2 ⊢n=C→F⁡n=F⁡C
12 11 eleq2d ⊢n=C→A∈F⁡n↔A∈F⁡C
13 oveq2 ⊢n=C→ABn=ABC
14 13 eleq1d ⊢n=C→ABn∈K↔ABC∈K
15 10 12 14 3anbi123d ⊢n=C→n∈ℕ0∧A∈F⁡n∧ABn∈K↔C∈ℕ0∧A∈F⁡C∧ABC∈K
16 4 5 9 15 3 brab ⊢AGC↔C∈ℕ0∧A∈F⁡C∧ABC∈K