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 | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }
heibor.4 
|- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }
heiborlem2.5 
|- A e. _V
heiborlem2.6 
|- C e. _V
Assertion heiborlem2 
|- ( A G C <-> ( C e. NN0 /\ A e. ( F ` C ) /\ ( A B C ) e. K ) )

Proof

Step Hyp Ref Expression
1 heibor.1 
 |-  J = ( MetOpen ` D )
2 heibor.3 
 |-  K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }
3 heibor.4 
 |-  G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }
4 heiborlem2.5 
 |-  A e. _V
5 heiborlem2.6 
 |-  C e. _V
6 eleq1 
 |-  ( y = A -> ( y e. ( F ` n ) <-> A e. ( F ` n ) ) )
7 oveq1 
 |-  ( y = A -> ( y B n ) = ( A B n ) )
8 7 eleq1d 
 |-  ( y = A -> ( ( y B n ) e. K <-> ( A B n ) e. K ) )
9 6 8 3anbi23d 
 |-  ( y = A -> ( ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) <-> ( n e. NN0 /\ A e. ( F ` n ) /\ ( A B n ) e. K ) ) )
10 eleq1 
 |-  ( n = C -> ( n e. NN0 <-> C e. NN0 ) )
11 fveq2 
 |-  ( n = C -> ( F ` n ) = ( F ` C ) )
12 11 eleq2d 
 |-  ( n = C -> ( A e. ( F ` n ) <-> A e. ( F ` C ) ) )
13 oveq2 
 |-  ( n = C -> ( A B n ) = ( A B C ) )
14 13 eleq1d 
 |-  ( n = C -> ( ( A B n ) e. K <-> ( A B C ) e. K ) )
15 10 12 14 3anbi123d 
 |-  ( n = C -> ( ( n e. NN0 /\ A e. ( F ` n ) /\ ( A B n ) e. K ) <-> ( C e. NN0 /\ A e. ( F ` C ) /\ ( A B C ) e. K ) ) )
16 4 5 9 15 3 brab 
 |-  ( A G C <-> ( C e. NN0 /\ A e. ( F ` C ) /\ ( A B C ) e. K ) )