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

Metamath Proof Explorer

Theorem axdc3lem3

Description: Simple substitution lemma for axdc3 . (Contributed by Mario Carneiro, 27-Jan-2013)

Ref Expression
Hypotheses axdc3lem3.1 
|- A e. _V
axdc3lem3.2 
|- S = { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
axdc3lem3.3 
|- B e. _V
Assertion axdc3lem3 
|- ( B e. S <-> E. m e. _om ( B : suc m --> A /\ ( B ` (/) ) = C /\ A. k e. m ( B ` suc k ) e. ( F ` ( B ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc3lem3.1 
 |-  A e. _V
2 axdc3lem3.2 
 |-  S = { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
3 axdc3lem3.3 
 |-  B e. _V
4 2 eleq2i 
 |-  ( B e. S <-> B e. { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } )
5 feq1 
 |-  ( s = B -> ( s : suc n --> A <-> B : suc n --> A ) )
6 fveq1 
 |-  ( s = B -> ( s ` (/) ) = ( B ` (/) ) )
7 6 eqeq1d 
 |-  ( s = B -> ( ( s ` (/) ) = C <-> ( B ` (/) ) = C ) )
8 fveq1 
 |-  ( s = B -> ( s ` suc k ) = ( B ` suc k ) )
9 fveq1 
 |-  ( s = B -> ( s ` k ) = ( B ` k ) )
10 9 fveq2d 
 |-  ( s = B -> ( F ` ( s ` k ) ) = ( F ` ( B ` k ) ) )
11 8 10 eleq12d 
 |-  ( s = B -> ( ( s ` suc k ) e. ( F ` ( s ` k ) ) <-> ( B ` suc k ) e. ( F ` ( B ` k ) ) ) )
12 11 ralbidv 
 |-  ( s = B -> ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) <-> A. k e. n ( B ` suc k ) e. ( F ` ( B ` k ) ) ) )
13 5 7 12 3anbi123d 
 |-  ( s = B -> ( ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) <-> ( B : suc n --> A /\ ( B ` (/) ) = C /\ A. k e. n ( B ` suc k ) e. ( F ` ( B ` k ) ) ) ) )
14 13 rexbidv 
 |-  ( s = B -> ( E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) <-> E. n e. _om ( B : suc n --> A /\ ( B ` (/) ) = C /\ A. k e. n ( B ` suc k ) e. ( F ` ( B ` k ) ) ) ) )
15 3 14 elab 
 |-  ( B e. { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } <-> E. n e. _om ( B : suc n --> A /\ ( B ` (/) ) = C /\ A. k e. n ( B ` suc k ) e. ( F ` ( B ` k ) ) ) )
16 suceq 
 |-  ( n = m -> suc n = suc m )
17 16 feq2d 
 |-  ( n = m -> ( B : suc n --> A <-> B : suc m --> A ) )
18 raleq 
 |-  ( n = m -> ( A. k e. n ( B ` suc k ) e. ( F ` ( B ` k ) ) <-> A. k e. m ( B ` suc k ) e. ( F ` ( B ` k ) ) ) )
19 17 18 3anbi13d 
 |-  ( n = m -> ( ( B : suc n --> A /\ ( B ` (/) ) = C /\ A. k e. n ( B ` suc k ) e. ( F ` ( B ` k ) ) ) <-> ( B : suc m --> A /\ ( B ` (/) ) = C /\ A. k e. m ( B ` suc k ) e. ( F ` ( B ` k ) ) ) ) )
20 19 cbvrexvw 
 |-  ( E. n e. _om ( B : suc n --> A /\ ( B ` (/) ) = C /\ A. k e. n ( B ` suc k ) e. ( F ` ( B ` k ) ) ) <-> E. m e. _om ( B : suc m --> A /\ ( B ` (/) ) = C /\ A. k e. m ( B ` suc k ) e. ( F ` ( B ` k ) ) ) )
21 4 15 20 3bitri 
 |-  ( B e. S <-> E. m e. _om ( B : suc m --> A /\ ( B ` (/) ) = C /\ A. k e. m ( B ` suc k ) e. ( F ` ( B ` k ) ) ) )