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 ⟶ 𝒫 V ∧ N ⊆ V ∧ I : A ⟶ 1-1 onto B ∧ ∀ i ∈ A H ⁡ I ⁡ i = F G ⁡ i → J ∈ B ∧ H ⁡ J ⊆ F N ↔ ∃ k ∈ A G ⁡ k ⊆ N ∧ I ⁡ k = J

Proof

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