Step |
Hyp |
Ref |
Expression |
1 |
|
prelpwi |
|- ( ( A e. X /\ B e. X ) -> { A , B } e. ~P X ) |
2 |
1
|
3adant1 |
|- ( ( X e. V /\ A e. X /\ B e. X ) -> { A , B } e. ~P X ) |
3 |
|
prfi |
|- { A , B } e. Fin |
4 |
3
|
a1i |
|- ( ( X e. V /\ A e. X /\ B e. X ) -> { A , B } e. Fin ) |
5 |
2 4
|
elind |
|- ( ( X e. V /\ A e. X /\ B e. X ) -> { A , B } e. ( ~P X i^i Fin ) ) |
6 |
|
intprg |
|- ( ( A e. X /\ B e. X ) -> |^| { A , B } = ( A i^i B ) ) |
7 |
6
|
3adant1 |
|- ( ( X e. V /\ A e. X /\ B e. X ) -> |^| { A , B } = ( A i^i B ) ) |
8 |
7
|
eqcomd |
|- ( ( X e. V /\ A e. X /\ B e. X ) -> ( A i^i B ) = |^| { A , B } ) |
9 |
|
inteq |
|- ( p = { A , B } -> |^| p = |^| { A , B } ) |
10 |
9
|
rspceeqv |
|- ( ( { A , B } e. ( ~P X i^i Fin ) /\ ( A i^i B ) = |^| { A , B } ) -> E. p e. ( ~P X i^i Fin ) ( A i^i B ) = |^| p ) |
11 |
5 8 10
|
syl2anc |
|- ( ( X e. V /\ A e. X /\ B e. X ) -> E. p e. ( ~P X i^i Fin ) ( A i^i B ) = |^| p ) |
12 |
|
inex1g |
|- ( A e. X -> ( A i^i B ) e. _V ) |
13 |
12
|
3ad2ant2 |
|- ( ( X e. V /\ A e. X /\ B e. X ) -> ( A i^i B ) e. _V ) |
14 |
|
simp1 |
|- ( ( X e. V /\ A e. X /\ B e. X ) -> X e. V ) |
15 |
|
elfi |
|- ( ( ( A i^i B ) e. _V /\ X e. V ) -> ( ( A i^i B ) e. ( fi ` X ) <-> E. p e. ( ~P X i^i Fin ) ( A i^i B ) = |^| p ) ) |
16 |
13 14 15
|
syl2anc |
|- ( ( X e. V /\ A e. X /\ B e. X ) -> ( ( A i^i B ) e. ( fi ` X ) <-> E. p e. ( ~P X i^i Fin ) ( A i^i B ) = |^| p ) ) |
17 |
11 16
|
mpbird |
|- ( ( X e. V /\ A e. X /\ B e. X ) -> ( A i^i B ) e. ( fi ` X ) ) |