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