Metamath Proof Explorer

Theorem onfrALTlem1

Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion onfrALTlem1 
|- ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ ( a i^i x ) = (/) ) -> E. y e. a ( a i^i y ) = (/) ) )

Proof

Step Hyp Ref Expression
1 19.8a 
 |-  ( ( x e. a /\ ( a i^i x ) = (/) ) -> E. x ( x e. a /\ ( a i^i x ) = (/) ) )
2 1 a1i 
 |-  ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ ( a i^i x ) = (/) ) -> E. x ( x e. a /\ ( a i^i x ) = (/) ) ) )
3 cbvexsv 
 |-  ( E. x ( x e. a /\ ( a i^i x ) = (/) ) <-> E. y [ y / x ] ( x e. a /\ ( a i^i x ) = (/) ) )
4 2 3 imbitrdi 
 |-  ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ ( a i^i x ) = (/) ) -> E. y [ y / x ] ( x e. a /\ ( a i^i x ) = (/) ) ) )
5 sbsbc 
 |-  ( [ y / x ] ( x e. a /\ ( a i^i x ) = (/) ) <-> [. y / x ]. ( x e. a /\ ( a i^i x ) = (/) ) )
6 onfrALTlem4 
 |-  ( [. y / x ]. ( x e. a /\ ( a i^i x ) = (/) ) <-> ( y e. a /\ ( a i^i y ) = (/) ) )
7 5 6 bitri 
 |-  ( [ y / x ] ( x e. a /\ ( a i^i x ) = (/) ) <-> ( y e. a /\ ( a i^i y ) = (/) ) )
8 7 exbii 
 |-  ( E. y [ y / x ] ( x e. a /\ ( a i^i x ) = (/) ) <-> E. y ( y e. a /\ ( a i^i y ) = (/) ) )
9 4 8 imbitrdi 
 |-  ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ ( a i^i x ) = (/) ) -> E. y ( y e. a /\ ( a i^i y ) = (/) ) ) )
10 df-rex 
 |-  ( E. y e. a ( a i^i y ) = (/) <-> E. y ( y e. a /\ ( a i^i y ) = (/) ) )
11 9 10 imbitrrdi 
 |-  ( ( a C_ On /\ a =/= (/) ) -> ( ( x e. a /\ ( a i^i x ) = (/) ) -> E. y e. a ( a i^i y ) = (/) ) )