Metamath Proof Explorer


Theorem isf34lem5

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Hypothesis compss.a
|- F = ( x e. ~P A |-> ( A \ x ) )
Assertion isf34lem5
|- ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` |^| X ) = U. ( F " X ) )

Proof

Step Hyp Ref Expression
1 compss.a
 |-  F = ( x e. ~P A |-> ( A \ x ) )
2 imassrn
 |-  ( F " X ) C_ ran F
3 1 isf34lem2
 |-  ( A e. V -> F : ~P A --> ~P A )
4 3 adantr
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> F : ~P A --> ~P A )
5 4 frnd
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ran F C_ ~P A )
6 2 5 sstrid
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F " X ) C_ ~P A )
7 simprl
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> X C_ ~P A )
8 4 fdmd
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> dom F = ~P A )
9 7 8 sseqtrrd
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> X C_ dom F )
10 sseqin2
 |-  ( X C_ dom F <-> ( dom F i^i X ) = X )
11 9 10 sylib
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( dom F i^i X ) = X )
12 simprr
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> X =/= (/) )
13 11 12 eqnetrd
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( dom F i^i X ) =/= (/) )
14 imadisj
 |-  ( ( F " X ) = (/) <-> ( dom F i^i X ) = (/) )
15 14 necon3bii
 |-  ( ( F " X ) =/= (/) <-> ( dom F i^i X ) =/= (/) )
16 13 15 sylibr
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F " X ) =/= (/) )
17 6 16 jca
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( ( F " X ) C_ ~P A /\ ( F " X ) =/= (/) ) )
18 1 isf34lem4
 |-  ( ( A e. V /\ ( ( F " X ) C_ ~P A /\ ( F " X ) =/= (/) ) ) -> ( F ` U. ( F " X ) ) = |^| ( F " ( F " X ) ) )
19 17 18 syldan
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` U. ( F " X ) ) = |^| ( F " ( F " X ) ) )
20 1 isf34lem3
 |-  ( ( A e. V /\ X C_ ~P A ) -> ( F " ( F " X ) ) = X )
21 20 adantrr
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F " ( F " X ) ) = X )
22 21 inteqd
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> |^| ( F " ( F " X ) ) = |^| X )
23 19 22 eqtrd
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` U. ( F " X ) ) = |^| X )
24 23 fveq2d
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` ( F ` U. ( F " X ) ) ) = ( F ` |^| X ) )
25 1 compsscnv
 |-  `' F = F
26 25 fveq1i
 |-  ( `' F ` ( F ` U. ( F " X ) ) ) = ( F ` ( F ` U. ( F " X ) ) )
27 1 compssiso
 |-  ( A e. V -> F Isom [C.] , `' [C.] ( ~P A , ~P A ) )
28 isof1o
 |-  ( F Isom [C.] , `' [C.] ( ~P A , ~P A ) -> F : ~P A -1-1-onto-> ~P A )
29 27 28 syl
 |-  ( A e. V -> F : ~P A -1-1-onto-> ~P A )
30 sspwuni
 |-  ( ( F " X ) C_ ~P A <-> U. ( F " X ) C_ A )
31 6 30 sylib
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> U. ( F " X ) C_ A )
32 elpw2g
 |-  ( A e. V -> ( U. ( F " X ) e. ~P A <-> U. ( F " X ) C_ A ) )
33 32 adantr
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( U. ( F " X ) e. ~P A <-> U. ( F " X ) C_ A ) )
34 31 33 mpbird
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> U. ( F " X ) e. ~P A )
35 f1ocnvfv1
 |-  ( ( F : ~P A -1-1-onto-> ~P A /\ U. ( F " X ) e. ~P A ) -> ( `' F ` ( F ` U. ( F " X ) ) ) = U. ( F " X ) )
36 29 34 35 syl2an2r
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( `' F ` ( F ` U. ( F " X ) ) ) = U. ( F " X ) )
37 26 36 eqtr3id
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` ( F ` U. ( F " X ) ) ) = U. ( F " X ) )
38 24 37 eqtr3d
 |-  ( ( A e. V /\ ( X C_ ~P A /\ X =/= (/) ) ) -> ( F ` |^| X ) = U. ( F " X ) )