This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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