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 ⊢ 𝐽 = ( 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 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐴 𝐵 𝐶 ) ∈ 𝐾 ) )