Metamath Proof Explorer

Theorem uhgrimisgrgriclem

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

Ref Expression
Assertion uhgrimisgrgriclem ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) → ( ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ↔ ∃ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑘 = ( ◡ 𝐼 ‘ 𝐽 ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) )
2 1 sseq1d ⊢ ( 𝑘 = ( ◡ 𝐼 ‘ 𝐽 ) → ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ↔ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) )
3 fveqeq2 ⊢ ( 𝑘 = ( ◡ 𝐼 ‘ 𝐽 ) → ( ( 𝐼 ‘ 𝑘 ) = 𝐽 ↔ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) = 𝐽 ) )
4 2 3 anbi12d ⊢ ( 𝑘 = ( ◡ 𝐼 ‘ 𝐽 ) → ( ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ↔ ( ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ∧ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) = 𝐽 ) ) )
5 simpr ⊢ ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐼 : 𝐴 –1-1-onto→ 𝐵 )
6 5 3ad2ant2 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) → 𝐼 : 𝐴 –1-1-onto→ 𝐵 )
7 simpl ⊢ ( ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) → 𝐽 ∈ 𝐵 )
8 f1ocnvdm ⊢ ( ( 𝐼 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐽 ∈ 𝐵 ) → ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 )
9 6 7 8 syl2an ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) → ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 )
10 2fveq3 ⊢ ( 𝑖 = ( ◡ 𝐼 ‘ 𝐽 ) → ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐻 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) )
11 fveq2 ⊢ ( 𝑖 = ( ◡ 𝐼 ‘ 𝐽 ) → ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) )
12 11 imaeq2d ⊢ ( 𝑖 = ( ◡ 𝐼 ‘ 𝐽 ) → ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) )
13 10 12 eqeq12d ⊢ ( 𝑖 = ( ◡ 𝐼 ‘ 𝐽 ) → ( ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ↔ ( 𝐻 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ) )
14 13 rspcv ⊢ ( ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 → ( ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) → ( 𝐻 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ) )
15 14 adantl ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) → ( ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) → ( 𝐻 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ) )
16 7 adantl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) → 𝐽 ∈ 𝐵 )
17 f1ocnvfv2 ⊢ ( ( 𝐼 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐽 ∈ 𝐵 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) = 𝐽 )
18 5 16 17 syl2anr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) = 𝐽 )
19 18 fveqeq2d ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → ( ( 𝐻 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ↔ ( 𝐻 ‘ 𝐽 ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ) )
20 sseq1 ⊢ ( ( 𝐻 ‘ 𝐽 ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) → ( ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ↔ ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ⊆ ( 𝐹 “ 𝑁 ) ) )
21 20 adantl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝐽 ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ) → ( ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ↔ ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ⊆ ( 𝐹 “ 𝑁 ) ) )
22 f1of1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 –1-1→ 𝑊 )
23 22 adantr ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) → 𝐹 : 𝑉 –1-1→ 𝑊 )
24 23 adantr ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) → 𝐹 : 𝑉 –1-1→ 𝑊 )
25 24 3ad2ant1 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → 𝐹 : 𝑉 –1-1→ 𝑊 )
26 simp1lr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → 𝐺 : 𝐴 ⟶ 𝒫 𝑉 )
27 simp1r ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 )
28 26 27 ffvelcdmd ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ∈ 𝒫 𝑉 )
29 28 elpwid ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑉 )
30 simpl ⊢ ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → 𝑁 ⊆ 𝑉 )
31 30 3ad2ant3 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → 𝑁 ⊆ 𝑉 )
32 f1imass ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑉 ∧ 𝑁 ⊆ 𝑉 ) ) → ( ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ⊆ ( 𝐹 “ 𝑁 ) ↔ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) )
33 25 29 31 32 syl12anc ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → ( ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ⊆ ( 𝐹 “ 𝑁 ) ↔ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) )
34 33 biimpd ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ 𝐽 ∈ 𝐵 ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → ( ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ⊆ ( 𝐹 “ 𝑁 ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) )
35 34 3exp ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) → ( 𝐽 ∈ 𝐵 → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ⊆ ( 𝐹 “ 𝑁 ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) ) )
36 35 com24 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) → ( ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ⊆ ( 𝐹 “ 𝑁 ) → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐽 ∈ 𝐵 → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) ) )
37 36 adantr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝐽 ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ) → ( ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ⊆ ( 𝐹 “ 𝑁 ) → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐽 ∈ 𝐵 → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) ) )
38 21 37 sylbid ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ ( 𝐻 ‘ 𝐽 ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) ) → ( ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐽 ∈ 𝐵 → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) ) )
39 38 ex ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝐽 ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) → ( ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐽 ∈ 𝐵 → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) ) ) )
40 39 com25 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) → ( 𝐽 ∈ 𝐵 → ( ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( ( 𝐻 ‘ 𝐽 ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) ) ) )
41 40 imp42 ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → ( ( 𝐻 ‘ 𝐽 ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) )
42 19 41 sylbid ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → ( ( 𝐻 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) )
43 42 ex ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( ( 𝐻 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) )
44 43 com23 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) → ( ( 𝐻 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) )
45 44 ex ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) → ( ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) → ( ( 𝐻 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) ) )
46 45 com23 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) → ( ( 𝐻 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) = ( 𝐹 “ ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ) → ( ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) ) )
47 15 46 syld ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 ) → ( ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) → ( ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) ) )
48 47 ex ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) → ( ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 → ( ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) → ( ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) ) ) )
49 48 com25 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) → ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → ( ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) → ( ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) → ( ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) ) ) ) )
50 49 3imp1 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) → ( ( ◡ 𝐼 ‘ 𝐽 ) ∈ 𝐴 → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ) )
51 9 50 mpd ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) → ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 )
52 6 7 17 syl2an ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) = 𝐽 )
53 51 52 jca ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) → ( ( 𝐺 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) ⊆ 𝑁 ∧ ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝐽 ) ) = 𝐽 ) )
54 4 9 53 rspcedvdw ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) ∧ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) → ∃ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) )
55 54 ex ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) → ( ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) → ∃ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ) )
56 f1of ⊢ ( 𝐼 : 𝐴 –1-1-onto→ 𝐵 → 𝐼 : 𝐴 ⟶ 𝐵 )
57 56 adantl ⊢ ( ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) → 𝐼 : 𝐴 ⟶ 𝐵 )
58 57 3ad2ant2 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) → 𝐼 : 𝐴 ⟶ 𝐵 )
59 58 3ad2ant1 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝐴 ∧ ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ) → 𝐼 : 𝐴 ⟶ 𝐵 )
60 simp2 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝐴 ∧ ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ) → 𝑘 ∈ 𝐴 )
61 59 60 ffvelcdmd ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝐴 ∧ ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ) → ( 𝐼 ‘ 𝑘 ) ∈ 𝐵 )
62 2fveq3 ⊢ ( 𝑖 = 𝑘 → ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) )
63 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝐺 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑘 ) )
64 63 imaeq2d ⊢ ( 𝑖 = 𝑘 → ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) )
65 62 64 eqeq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ↔ ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) ) )
66 65 rspcv ⊢ ( 𝑘 ∈ 𝐴 → ( ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) → ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) ) )
67 66 adantl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) → ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) ) )
68 simp3 ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ∧ ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) ) → ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) )
69 imass2 ⊢ ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 → ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) )
70 69 adantr ⊢ ( ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) → ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) )
71 70 3ad2ant2 ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ∧ ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) ) → ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) )
72 68 71 eqsstrd ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) ∧ ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ∧ ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) ) → ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) )
73 72 3exp ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) → ( ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) → ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) ) ) )
74 73 com23 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑘 ) ) → ( ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) → ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) ) ) )
75 67 74 syld ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) → ( ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) → ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) ) ) )
76 75 ex ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → ( 𝑘 ∈ 𝐴 → ( ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) → ( ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) → ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) ) ) ) )
77 76 com23 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ) → ( ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) → ( 𝑘 ∈ 𝐴 → ( ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) → ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) ) ) ) )
78 77 3impia ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) → ( 𝑘 ∈ 𝐴 → ( ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) → ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) ) ) )
79 78 3imp ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝐴 ∧ ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ) → ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) )
80 eleq1 ⊢ ( ( 𝐼 ‘ 𝑘 ) = 𝐽 → ( ( 𝐼 ‘ 𝑘 ) ∈ 𝐵 ↔ 𝐽 ∈ 𝐵 ) )
81 fveq2 ⊢ ( ( 𝐼 ‘ 𝑘 ) = 𝐽 → ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) = ( 𝐻 ‘ 𝐽 ) )
82 81 sseq1d ⊢ ( ( 𝐼 ‘ 𝑘 ) = 𝐽 → ( ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) ↔ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) )
83 80 82 anbi12d ⊢ ( ( 𝐼 ‘ 𝑘 ) = 𝐽 → ( ( ( 𝐼 ‘ 𝑘 ) ∈ 𝐵 ∧ ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) ) ↔ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) )
84 83 adantl ⊢ ( ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) → ( ( ( 𝐼 ‘ 𝑘 ) ∈ 𝐵 ∧ ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) ) ↔ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) )
85 84 3ad2ant3 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝐴 ∧ ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ) → ( ( ( 𝐼 ‘ 𝑘 ) ∈ 𝐵 ∧ ( 𝐻 ‘ ( 𝐼 ‘ 𝑘 ) ) ⊆ ( 𝐹 “ 𝑁 ) ) ↔ ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) )
86 61 79 85 mpbi2and ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) ∧ 𝑘 ∈ 𝐴 ∧ ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ) → ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) )
87 86 rexlimdv3a ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) → ( ∃ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) → ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) )
88 55 87 impbid ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝐺 : 𝐴 ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝐼 : 𝐴 –1-1-onto→ 𝐵 ) ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐻 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 ‘ 𝑖 ) ) ) → ( ( 𝐽 ∈ 𝐵 ∧ ( 𝐻 ‘ 𝐽 ) ⊆ ( 𝐹 “ 𝑁 ) ) ↔ ∃ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝐼 ‘ 𝑘 ) = 𝐽 ) ) )