This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∩ Fin u ⊆ ⋃ v
heibor.4 ⊢ G = y n | n ∈ ℕ 0 ∧ y ∈ F ⁡ n ∧ y B n ∈ K
heiborlem2.5 ⊢ A ∈ V
heiborlem2.6 ⊢ C ∈ V
Assertion heiborlem2 ⊢ A G C ↔ C ∈ ℕ 0 ∧ A ∈ F ⁡ C ∧ A B C ∈ K

Proof

Step Hyp Ref Expression
1 heibor.1 ⊢ J = MetOpen ⁡ D
2 heibor.3 ⊢ K = u | ¬ ∃ v ∈ 𝒫 U ∩ Fin u ⊆ ⋃ v
3 heibor.4 ⊢ G = y n | n ∈ ℕ 0 ∧ y ∈ F ⁡ n ∧ y B n ∈ 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 → y B n = A B n
8 7 eleq1d ⊢ y = A → y B n ∈ K ↔ A B n ∈ K
9 6 8 3anbi23d ⊢ y = A → n ∈ ℕ 0 ∧ y ∈ F ⁡ n ∧ y B n ∈ K ↔ n ∈ ℕ 0 ∧ A ∈ F ⁡ n ∧ A B n ∈ 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 → A B n = A B C
14 13 eleq1d ⊢ n = C → A B n ∈ K ↔ A B C ∈ K
15 10 12 14 3anbi123d ⊢ n = C → n ∈ ℕ 0 ∧ A ∈ F ⁡ n ∧ A B n ∈ K ↔ C ∈ ℕ 0 ∧ A ∈ F ⁡ C ∧ A B C ∈ K
16 4 5 9 15 3 brab ⊢ A G C ↔ C ∈ ℕ 0 ∧ A ∈ F ⁡ C ∧ A B C ∈ K