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

Metamath Proof Explorer

Theorem uhgrimisgrgriclem

Description: Lemma for uhgrimisgrgric . (Contributed by AV, 31-May-2025)

Ref Expression
Assertion uhgrimisgrgriclem 
|- ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) -> ( ( J e. B /\ ( H ` J ) C_ ( F " N ) ) <-> E. k e. A ( ( G ` k ) C_ N /\ ( I ` k ) = J ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( k = ( `' I ` J ) -> ( G ` k ) = ( G ` ( `' I ` J ) ) )
2 1 sseq1d 
 |-  ( k = ( `' I ` J ) -> ( ( G ` k ) C_ N <-> ( G ` ( `' I ` J ) ) C_ N ) )
3 fveqeq2 
 |-  ( k = ( `' I ` J ) -> ( ( I ` k ) = J <-> ( I ` ( `' I ` J ) ) = J ) )
4 2 3 anbi12d 
 |-  ( k = ( `' I ` J ) -> ( ( ( G ` k ) C_ N /\ ( I ` k ) = J ) <-> ( ( G ` ( `' I ` J ) ) C_ N /\ ( I ` ( `' I ` J ) ) = J ) ) )
5 simpr 
 |-  ( ( N C_ V /\ I : A -1-1-onto-> B ) -> I : A -1-1-onto-> B )
6 5 3ad2ant2 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) -> I : A -1-1-onto-> B )
7 simpl 
 |-  ( ( J e. B /\ ( H ` J ) C_ ( F " N ) ) -> J e. B )
8 f1ocnvdm 
 |-  ( ( I : A -1-1-onto-> B /\ J e. B ) -> ( `' I ` J ) e. A )
9 6 7 8 syl2an 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) -> ( `' I ` J ) e. A )
10 2fveq3 
 |-  ( i = ( `' I ` J ) -> ( H ` ( I ` i ) ) = ( H ` ( I ` ( `' I ` J ) ) ) )
11 fveq2 
 |-  ( i = ( `' I ` J ) -> ( G ` i ) = ( G ` ( `' I ` J ) ) )
12 11 imaeq2d 
 |-  ( i = ( `' I ` J ) -> ( F " ( G ` i ) ) = ( F " ( G ` ( `' I ` J ) ) ) )
13 10 12 eqeq12d 
 |-  ( i = ( `' I ` J ) -> ( ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) <-> ( H ` ( I ` ( `' I ` J ) ) ) = ( F " ( G ` ( `' I ` J ) ) ) ) )
14 13 rspcv 
 |-  ( ( `' I ` J ) e. A -> ( A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) -> ( H ` ( I ` ( `' I ` J ) ) ) = ( F " ( G ` ( `' I ` J ) ) ) ) )
15 14 adantl 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) -> ( A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) -> ( H ` ( I ` ( `' I ` J ) ) ) = ( F " ( G ` ( `' I ` J ) ) ) ) )
16 7 adantl 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) -> J e. B )
17 f1ocnvfv2 
 |-  ( ( I : A -1-1-onto-> B /\ J e. B ) -> ( I ` ( `' I ` J ) ) = J )
18 5 16 17 syl2anr 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> ( I ` ( `' I ` J ) ) = J )
19 18 fveqeq2d 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> ( ( H ` ( I ` ( `' I ` J ) ) ) = ( F " ( G ` ( `' I ` J ) ) ) <-> ( H ` J ) = ( F " ( G ` ( `' I ` J ) ) ) ) )
20 sseq1 
 |-  ( ( H ` J ) = ( F " ( G ` ( `' I ` J ) ) ) -> ( ( H ` J ) C_ ( F " N ) <-> ( F " ( G ` ( `' I ` J ) ) ) C_ ( F " N ) ) )
21 20 adantl 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ ( H ` J ) = ( F " ( G ` ( `' I ` J ) ) ) ) -> ( ( H ` J ) C_ ( F " N ) <-> ( F " ( G ` ( `' I ` J ) ) ) C_ ( F " N ) ) )
22 f1of1 
 |-  ( F : V -1-1-onto-> W -> F : V -1-1-> W )
23 22 adantr 
 |-  ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) -> F : V -1-1-> W )
24 23 adantr 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) -> F : V -1-1-> W )
25 24 3ad2ant1 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ J e. B /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> F : V -1-1-> W )
26 simp1lr 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ J e. B /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> G : A --> ~P V )
27 simp1r 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ J e. B /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> ( `' I ` J ) e. A )
28 26 27 ffvelcdmd 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ J e. B /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> ( G ` ( `' I ` J ) ) e. ~P V )
29 28 elpwid 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ J e. B /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> ( G ` ( `' I ` J ) ) C_ V )
30 simpl 
 |-  ( ( N C_ V /\ I : A -1-1-onto-> B ) -> N C_ V )
31 30 3ad2ant3 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ J e. B /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> N C_ V )
32 f1imass 
 |-  ( ( F : V -1-1-> W /\ ( ( G ` ( `' I ` J ) ) C_ V /\ N C_ V ) ) -> ( ( F " ( G ` ( `' I ` J ) ) ) C_ ( F " N ) <-> ( G ` ( `' I ` J ) ) C_ N ) )
33 25 29 31 32 syl12anc 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ J e. B /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> ( ( F " ( G ` ( `' I ` J ) ) ) C_ ( F " N ) <-> ( G ` ( `' I ` J ) ) C_ N ) )
34 33 biimpd 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ J e. B /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> ( ( F " ( G ` ( `' I ` J ) ) ) C_ ( F " N ) -> ( G ` ( `' I ` J ) ) C_ N ) )
35 34 3exp 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) -> ( J e. B -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( ( F " ( G ` ( `' I ` J ) ) ) C_ ( F " N ) -> ( G ` ( `' I ` J ) ) C_ N ) ) ) )
36 35 com24 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) -> ( ( F " ( G ` ( `' I ` J ) ) ) C_ ( F " N ) -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( J e. B -> ( G ` ( `' I ` J ) ) C_ N ) ) ) )
37 36 adantr 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ ( H ` J ) = ( F " ( G ` ( `' I ` J ) ) ) ) -> ( ( F " ( G ` ( `' I ` J ) ) ) C_ ( F " N ) -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( J e. B -> ( G ` ( `' I ` J ) ) C_ N ) ) ) )
38 21 37 sylbid 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ ( H ` J ) = ( F " ( G ` ( `' I ` J ) ) ) ) -> ( ( H ` J ) C_ ( F " N ) -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( J e. B -> ( G ` ( `' I ` J ) ) C_ N ) ) ) )
39 38 ex 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) -> ( ( H ` J ) = ( F " ( G ` ( `' I ` J ) ) ) -> ( ( H ` J ) C_ ( F " N ) -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( J e. B -> ( G ` ( `' I ` J ) ) C_ N ) ) ) ) )
40 39 com25 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) -> ( J e. B -> ( ( H ` J ) C_ ( F " N ) -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( ( H ` J ) = ( F " ( G ` ( `' I ` J ) ) ) -> ( G ` ( `' I ` J ) ) C_ N ) ) ) ) )
41 40 imp42 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> ( ( H ` J ) = ( F " ( G ` ( `' I ` J ) ) ) -> ( G ` ( `' I ` J ) ) C_ N ) )
42 19 41 sylbid 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> ( ( H ` ( I ` ( `' I ` J ) ) ) = ( F " ( G ` ( `' I ` J ) ) ) -> ( G ` ( `' I ` J ) ) C_ N ) )
43 42 ex 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( ( H ` ( I ` ( `' I ` J ) ) ) = ( F " ( G ` ( `' I ` J ) ) ) -> ( G ` ( `' I ` J ) ) C_ N ) ) )
44 43 com23 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) -> ( ( H ` ( I ` ( `' I ` J ) ) ) = ( F " ( G ` ( `' I ` J ) ) ) -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( G ` ( `' I ` J ) ) C_ N ) ) )
45 44 ex 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) -> ( ( J e. B /\ ( H ` J ) C_ ( F " N ) ) -> ( ( H ` ( I ` ( `' I ` J ) ) ) = ( F " ( G ` ( `' I ` J ) ) ) -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( G ` ( `' I ` J ) ) C_ N ) ) ) )
46 45 com23 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) -> ( ( H ` ( I ` ( `' I ` J ) ) ) = ( F " ( G ` ( `' I ` J ) ) ) -> ( ( J e. B /\ ( H ` J ) C_ ( F " N ) ) -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( G ` ( `' I ` J ) ) C_ N ) ) ) )
47 15 46 syld 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( `' I ` J ) e. A ) -> ( A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) -> ( ( J e. B /\ ( H ` J ) C_ ( F " N ) ) -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( G ` ( `' I ` J ) ) C_ N ) ) ) )
48 47 ex 
 |-  ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) -> ( ( `' I ` J ) e. A -> ( A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) -> ( ( J e. B /\ ( H ` J ) C_ ( F " N ) ) -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( G ` ( `' I ` J ) ) C_ N ) ) ) ) )
49 48 com25 
 |-  ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) -> ( ( N C_ V /\ I : A -1-1-onto-> B ) -> ( A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) -> ( ( J e. B /\ ( H ` J ) C_ ( F " N ) ) -> ( ( `' I ` J ) e. A -> ( G ` ( `' I ` J ) ) C_ N ) ) ) ) )
50 49 3imp1 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) -> ( ( `' I ` J ) e. A -> ( G ` ( `' I ` J ) ) C_ N ) )
51 9 50 mpd 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) -> ( G ` ( `' I ` J ) ) C_ N )
52 6 7 17 syl2an 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) -> ( I ` ( `' I ` J ) ) = J )
53 51 52 jca 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) -> ( ( G ` ( `' I ` J ) ) C_ N /\ ( I ` ( `' I ` J ) ) = J ) )
54 4 9 53 rspcedvdw 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) /\ ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) -> E. k e. A ( ( G ` k ) C_ N /\ ( I ` k ) = J ) )
55 54 ex 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) -> ( ( J e. B /\ ( H ` J ) C_ ( F " N ) ) -> E. k e. A ( ( G ` k ) C_ N /\ ( I ` k ) = J ) ) )
56 f1of 
 |-  ( I : A -1-1-onto-> B -> I : A --> B )
57 56 adantl 
 |-  ( ( N C_ V /\ I : A -1-1-onto-> B ) -> I : A --> B )
58 57 3ad2ant2 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) -> I : A --> B )
59 58 3ad2ant1 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) /\ k e. A /\ ( ( G ` k ) C_ N /\ ( I ` k ) = J ) ) -> I : A --> B )
60 simp2 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) /\ k e. A /\ ( ( G ` k ) C_ N /\ ( I ` k ) = J ) ) -> k e. A )
61 59 60 ffvelcdmd 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) /\ k e. A /\ ( ( G ` k ) C_ N /\ ( I ` k ) = J ) ) -> ( I ` k ) e. B )
62 2fveq3 
 |-  ( i = k -> ( H ` ( I ` i ) ) = ( H ` ( I ` k ) ) )
63 fveq2 
 |-  ( i = k -> ( G ` i ) = ( G ` k ) )
64 63 imaeq2d 
 |-  ( i = k -> ( F " ( G ` i ) ) = ( F " ( G ` k ) ) )
65 62 64 eqeq12d 
 |-  ( i = k -> ( ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) <-> ( H ` ( I ` k ) ) = ( F " ( G ` k ) ) ) )
66 65 rspcv 
 |-  ( k e. A -> ( A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) -> ( H ` ( I ` k ) ) = ( F " ( G ` k ) ) ) )
67 66 adantl 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) /\ k e. A ) -> ( A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) -> ( H ` ( I ` k ) ) = ( F " ( G ` k ) ) ) )
68 simp3 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) /\ k e. A ) /\ ( ( G ` k ) C_ N /\ ( I ` k ) = J ) /\ ( H ` ( I ` k ) ) = ( F " ( G ` k ) ) ) -> ( H ` ( I ` k ) ) = ( F " ( G ` k ) ) )
69 imass2 
 |-  ( ( G ` k ) C_ N -> ( F " ( G ` k ) ) C_ ( F " N ) )
70 69 adantr 
 |-  ( ( ( G ` k ) C_ N /\ ( I ` k ) = J ) -> ( F " ( G ` k ) ) C_ ( F " N ) )
71 70 3ad2ant2 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) /\ k e. A ) /\ ( ( G ` k ) C_ N /\ ( I ` k ) = J ) /\ ( H ` ( I ` k ) ) = ( F " ( G ` k ) ) ) -> ( F " ( G ` k ) ) C_ ( F " N ) )
72 68 71 eqsstrd 
 |-  ( ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) /\ k e. A ) /\ ( ( G ` k ) C_ N /\ ( I ` k ) = J ) /\ ( H ` ( I ` k ) ) = ( F " ( G ` k ) ) ) -> ( H ` ( I ` k ) ) C_ ( F " N ) )
73 72 3exp 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) /\ k e. A ) -> ( ( ( G ` k ) C_ N /\ ( I ` k ) = J ) -> ( ( H ` ( I ` k ) ) = ( F " ( G ` k ) ) -> ( H ` ( I ` k ) ) C_ ( F " N ) ) ) )
74 73 com23 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) /\ k e. A ) -> ( ( H ` ( I ` k ) ) = ( F " ( G ` k ) ) -> ( ( ( G ` k ) C_ N /\ ( I ` k ) = J ) -> ( H ` ( I ` k ) ) C_ ( F " N ) ) ) )
75 67 74 syld 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) /\ k e. A ) -> ( A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) -> ( ( ( G ` k ) C_ N /\ ( I ` k ) = J ) -> ( H ` ( I ` k ) ) C_ ( F " N ) ) ) )
76 75 ex 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> ( k e. A -> ( A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) -> ( ( ( G ` k ) C_ N /\ ( I ` k ) = J ) -> ( H ` ( I ` k ) ) C_ ( F " N ) ) ) ) )
77 76 com23 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) ) -> ( A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) -> ( k e. A -> ( ( ( G ` k ) C_ N /\ ( I ` k ) = J ) -> ( H ` ( I ` k ) ) C_ ( F " N ) ) ) ) )
78 77 3impia 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) -> ( k e. A -> ( ( ( G ` k ) C_ N /\ ( I ` k ) = J ) -> ( H ` ( I ` k ) ) C_ ( F " N ) ) ) )
79 78 3imp 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) /\ k e. A /\ ( ( G ` k ) C_ N /\ ( I ` k ) = J ) ) -> ( H ` ( I ` k ) ) C_ ( F " N ) )
80 eleq1 
 |-  ( ( I ` k ) = J -> ( ( I ` k ) e. B <-> J e. B ) )
81 fveq2 
 |-  ( ( I ` k ) = J -> ( H ` ( I ` k ) ) = ( H ` J ) )
82 81 sseq1d 
 |-  ( ( I ` k ) = J -> ( ( H ` ( I ` k ) ) C_ ( F " N ) <-> ( H ` J ) C_ ( F " N ) ) )
83 80 82 anbi12d 
 |-  ( ( I ` k ) = J -> ( ( ( I ` k ) e. B /\ ( H ` ( I ` k ) ) C_ ( F " N ) ) <-> ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) )
84 83 adantl 
 |-  ( ( ( G ` k ) C_ N /\ ( I ` k ) = J ) -> ( ( ( I ` k ) e. B /\ ( H ` ( I ` k ) ) C_ ( F " N ) ) <-> ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) )
85 84 3ad2ant3 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) /\ k e. A /\ ( ( G ` k ) C_ N /\ ( I ` k ) = J ) ) -> ( ( ( I ` k ) e. B /\ ( H ` ( I ` k ) ) C_ ( F " N ) ) <-> ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) )
86 61 79 85 mpbi2and 
 |-  ( ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) /\ k e. A /\ ( ( G ` k ) C_ N /\ ( I ` k ) = J ) ) -> ( J e. B /\ ( H ` J ) C_ ( F " N ) ) )
87 86 rexlimdv3a 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) -> ( E. k e. A ( ( G ` k ) C_ N /\ ( I ` k ) = J ) -> ( J e. B /\ ( H ` J ) C_ ( F " N ) ) ) )
88 55 87 impbid 
 |-  ( ( ( F : V -1-1-onto-> W /\ G : A --> ~P V ) /\ ( N C_ V /\ I : A -1-1-onto-> B ) /\ A. i e. A ( H ` ( I ` i ) ) = ( F " ( G ` i ) ) ) -> ( ( J e. B /\ ( H ` J ) C_ ( F " N ) ) <-> E. k e. A ( ( G ` k ) C_ N /\ ( I ` k ) = J ) ) )