Metamath Proof Explorer

Theorem imasubc3lem1

Description: Lemma for imasubc3 . (Contributed by Zhi Wang, 7-Nov-2025)

Ref Expression
Hypotheses imasubc3lem1.s 
|- S = ( F " A )
imasubc3lem1.f 
|- ( ph -> F : B -1-1-> C )
imasubc3lem1.x 
|- ( ph -> X e. S )
Assertion imasubc3lem1 
|- ( ph -> ( { ( `' F ` X ) } = ( `' F " { X } ) /\ ( F ` ( `' F ` X ) ) = X /\ ( `' F ` X ) e. B ) )

Proof

Step Hyp Ref Expression
1 imasubc3lem1.s 
 |-  S = ( F " A )
2 imasubc3lem1.f 
 |-  ( ph -> F : B -1-1-> C )
3 imasubc3lem1.x 
 |-  ( ph -> X e. S )
4 f1f1orn 
 |-  ( F : B -1-1-> C -> F : B -1-1-onto-> ran F )
5 2 4 syl 
 |-  ( ph -> F : B -1-1-onto-> ran F )
6 dff1o4 
 |-  ( F : B -1-1-onto-> ran F <-> ( F Fn B /\ `' F Fn ran F ) )
7 6 simprbi 
 |-  ( F : B -1-1-onto-> ran F -> `' F Fn ran F )
8 5 7 syl 
 |-  ( ph -> `' F Fn ran F )
9 imassrn 
 |-  ( F " A ) C_ ran F
10 3 1 eleqtrdi 
 |-  ( ph -> X e. ( F " A ) )
11 9 10 sselid 
 |-  ( ph -> X e. ran F )
12 fnsnfv 
 |-  ( ( `' F Fn ran F /\ X e. ran F ) -> { ( `' F ` X ) } = ( `' F " { X } ) )
13 8 11 12 syl2anc 
 |-  ( ph -> { ( `' F ` X ) } = ( `' F " { X } ) )
14 f1ocnvfv2 
 |-  ( ( F : B -1-1-onto-> ran F /\ X e. ran F ) -> ( F ` ( `' F ` X ) ) = X )
15 5 11 14 syl2anc 
 |-  ( ph -> ( F ` ( `' F ` X ) ) = X )
16 f1ocnvdm 
 |-  ( ( F : B -1-1-onto-> ran F /\ X e. ran F ) -> ( `' F ` X ) e. B )
17 5 11 16 syl2anc 
 |-  ( ph -> ( `' F ` X ) e. B )
18 13 15 17 3jca 
 |-  ( ph -> ( { ( `' F ` X ) } = ( `' F " { X } ) /\ ( F ` ( `' F ` X ) ) = X /\ ( `' F ` X ) e. B ) )