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 ) )