Metamath Proof Explorer

Theorem erdszelem1

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypothesis erdszelem1.1 
|- S = { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) }
Assertion erdszelem1 
|- ( X e. S <-> ( X C_ ( 1 ... A ) /\ ( F |` X ) Isom < , O ( X , ( F " X ) ) /\ A e. X ) )

Proof

Step Hyp Ref Expression
1 erdszelem1.1 
 |-  S = { y e. ~P ( 1 ... A ) | ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) }
2 ovex 
 |-  ( 1 ... A ) e. _V
3 2 elpw2 
 |-  ( X e. ~P ( 1 ... A ) <-> X C_ ( 1 ... A ) )
4 3 anbi1i 
 |-  ( ( X e. ~P ( 1 ... A ) /\ ( ( F |` X ) Isom < , O ( X , ( F " X ) ) /\ A e. X ) ) <-> ( X C_ ( 1 ... A ) /\ ( ( F |` X ) Isom < , O ( X , ( F " X ) ) /\ A e. X ) ) )
5 reseq2 
 |-  ( y = X -> ( F |` y ) = ( F |` X ) )
6 isoeq1 
 |-  ( ( F |` y ) = ( F |` X ) -> ( ( F |` y ) Isom < , O ( y , ( F " y ) ) <-> ( F |` X ) Isom < , O ( y , ( F " y ) ) ) )
7 5 6 syl 
 |-  ( y = X -> ( ( F |` y ) Isom < , O ( y , ( F " y ) ) <-> ( F |` X ) Isom < , O ( y , ( F " y ) ) ) )
8 isoeq4 
 |-  ( y = X -> ( ( F |` X ) Isom < , O ( y , ( F " y ) ) <-> ( F |` X ) Isom < , O ( X , ( F " y ) ) ) )
9 imaeq2 
 |-  ( y = X -> ( F " y ) = ( F " X ) )
10 isoeq5 
 |-  ( ( F " y ) = ( F " X ) -> ( ( F |` X ) Isom < , O ( X , ( F " y ) ) <-> ( F |` X ) Isom < , O ( X , ( F " X ) ) ) )
11 9 10 syl 
 |-  ( y = X -> ( ( F |` X ) Isom < , O ( X , ( F " y ) ) <-> ( F |` X ) Isom < , O ( X , ( F " X ) ) ) )
12 7 8 11 3bitrd 
 |-  ( y = X -> ( ( F |` y ) Isom < , O ( y , ( F " y ) ) <-> ( F |` X ) Isom < , O ( X , ( F " X ) ) ) )
13 eleq2 
 |-  ( y = X -> ( A e. y <-> A e. X ) )
14 12 13 anbi12d 
 |-  ( y = X -> ( ( ( F |` y ) Isom < , O ( y , ( F " y ) ) /\ A e. y ) <-> ( ( F |` X ) Isom < , O ( X , ( F " X ) ) /\ A e. X ) ) )
15 14 1 elrab2 
 |-  ( X e. S <-> ( X e. ~P ( 1 ... A ) /\ ( ( F |` X ) Isom < , O ( X , ( F " X ) ) /\ A e. X ) ) )
16 3anass 
 |-  ( ( X C_ ( 1 ... A ) /\ ( F |` X ) Isom < , O ( X , ( F " X ) ) /\ A e. X ) <-> ( X C_ ( 1 ... A ) /\ ( ( F |` X ) Isom < , O ( X , ( F " X ) ) /\ A e. X ) ) )
17 4 15 16 3bitr4i 
 |-  ( X e. S <-> ( X C_ ( 1 ... A ) /\ ( F |` X ) Isom < , O ( X , ( F " X ) ) /\ A e. X ) )