Metamath Proof Explorer

Theorem elfir

Description: Sufficient condition for an element of ( fiB ) . (Contributed by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion elfir 
|- ( ( B e. V /\ ( A C_ B /\ A =/= (/) /\ A e. Fin ) ) -> |^| A e. ( fi ` B ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A C_ B /\ A =/= (/) /\ A e. Fin ) -> A C_ B )
2 elpw2g 
 |-  ( B e. V -> ( A e. ~P B <-> A C_ B ) )
3 1 2 syl5ibr 
 |-  ( B e. V -> ( ( A C_ B /\ A =/= (/) /\ A e. Fin ) -> A e. ~P B ) )
4 3 imp 
 |-  ( ( B e. V /\ ( A C_ B /\ A =/= (/) /\ A e. Fin ) ) -> A e. ~P B )
5 simpr3 
 |-  ( ( B e. V /\ ( A C_ B /\ A =/= (/) /\ A e. Fin ) ) -> A e. Fin )
6 4 5 elind 
 |-  ( ( B e. V /\ ( A C_ B /\ A =/= (/) /\ A e. Fin ) ) -> A e. ( ~P B i^i Fin ) )
7 eqid 
 |-  |^| A = |^| A
8 inteq 
 |-  ( x = A -> |^| x = |^| A )
9 8 rspceeqv 
 |-  ( ( A e. ( ~P B i^i Fin ) /\ |^| A = |^| A ) -> E. x e. ( ~P B i^i Fin ) |^| A = |^| x )
10 6 7 9 sylancl 
 |-  ( ( B e. V /\ ( A C_ B /\ A =/= (/) /\ A e. Fin ) ) -> E. x e. ( ~P B i^i Fin ) |^| A = |^| x )
11 simp2 
 |-  ( ( A C_ B /\ A =/= (/) /\ A e. Fin ) -> A =/= (/) )
12 intex 
 |-  ( A =/= (/) <-> |^| A e. _V )
13 11 12 sylib 
 |-  ( ( A C_ B /\ A =/= (/) /\ A e. Fin ) -> |^| A e. _V )
14 id 
 |-  ( B e. V -> B e. V )
15 elfi 
 |-  ( ( |^| A e. _V /\ B e. V ) -> ( |^| A e. ( fi ` B ) <-> E. x e. ( ~P B i^i Fin ) |^| A = |^| x ) )
16 13 14 15 syl2anr 
 |-  ( ( B e. V /\ ( A C_ B /\ A =/= (/) /\ A e. Fin ) ) -> ( |^| A e. ( fi ` B ) <-> E. x e. ( ~P B i^i Fin ) |^| A = |^| x ) )
17 10 16 mpbird 
 |-  ( ( B e. V /\ ( A C_ B /\ A =/= (/) /\ A e. Fin ) ) -> |^| A e. ( fi ` B ) )