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