Theorem uhgrimisgrgriclem 49295

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

Assertion

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

Distinct variable groups:   𝐴,𝑖,𝑘   𝐵,𝑘   𝑖,𝐹,𝑘   𝑖,𝐺,𝑘   𝑖,𝐻,𝑘   𝑖,𝐼,𝑘   𝑖,𝐽,𝑘   𝑘,𝑁   𝑘,𝑉   𝑘,𝑊

Allowed substitution hints:   𝐵(𝑖)   𝑁(𝑖)   𝑉(𝑖)   𝑊(𝑖)

Proof of Theorem uhgrimisgrgriclem

Step	Hyp	Ref	Expression
1		fveq2 6914	. . . . . 6 ⊢ (𝑘 = (◡𝐼‘𝐽) → (𝐺‘𝑘) = (𝐺‘(◡𝐼‘𝐽)))
2	1	sseq1d 3944	. . . . 5 ⊢ (𝑘 = (◡𝐼‘𝐽) → ((𝐺‘𝑘) ⊆ 𝑁 ↔ (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))
3		fveqeq2 6923	. . . . 5 ⊢ (𝑘 = (◡𝐼‘𝐽) → ((𝐼‘𝑘) = 𝐽 ↔ (𝐼‘(◡𝐼‘𝐽)) = 𝐽))
4	2, 3	anbi12d 644	. . . 4 ⊢ (𝑘 = (◡𝐼‘𝐽) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ↔ ((𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁 ∧ (𝐼‘(◡𝐼‘𝐽)) = 𝐽)))
5		simpr 490	. . . . . 6 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → 𝐼:𝐴⟶1-1onto𝐵)
6	5	3ad2ant2 1152	. . . . 5 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → 𝐼:𝐴⟶1-1onto𝐵)
7		simpl 488	. . . . 5 ⊢ ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → 𝐽 ∈ 𝐵)
8		f1ocnvdm 7322	. . . . 5 ⊢ ((𝐼:𝐴⟶1-1onto𝐵 ∧ 𝐽 ∈ 𝐵) → (◡𝐼‘𝐽) ∈ 𝐴)
9	6, 7, 8	syl2an 608	. . . 4 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (◡𝐼‘𝐽) ∈ 𝐴)
10		2fveq3 6919	. . . . . . . . . . . . 13 ⊢ (𝑖 = (◡𝐼‘𝐽) → (𝐻‘(𝐼‘𝑖)) = (𝐻‘(𝐼‘(◡𝐼‘𝐽))))
11		fveq2 6914	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (◡𝐼‘𝐽) → (𝐺‘𝑖) = (𝐺‘(◡𝐼‘𝐽)))
12	11	imaeq2d 6068	. . . . . . . . . . . . 13 ⊢ (𝑖 = (◡𝐼‘𝐽) → (𝐹 “ (𝐺‘𝑖)) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽))))
13	10, 12	eqeq12d 2779	. . . . . . . . . . . 12 ⊢ (𝑖 = (◡𝐼‘𝐽) → ((𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) ↔ (𝐻‘(𝐼‘(◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽)))))
14	13	rspcv 3576	. . . . . . . . . . 11 ⊢ ((◡𝐼‘𝐽) ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘(◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽)))))
15	14	adantl 487	. . . . . . . . . 10 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘(◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽)))))
16	7	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → 𝐽 ∈ 𝐵)
17		f1ocnvfv2 7314	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼:𝐴⟶1-1onto𝐵 ∧ 𝐽 ∈ 𝐵) → (𝐼‘(◡𝐼‘𝐽)) = 𝐽)
18	5, 16, 17	syl2anr 609	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → (𝐼‘(◡𝐼‘𝐽)) = 𝐽)
19	18	fveqeq2d 6922	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → ((𝐻‘(𝐼‘(◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽))) ↔ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽)))))
20		sseq1 3938	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) ↔ (𝐹 “ (𝐺‘(◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁)))
21	20	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽)))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) ↔ (𝐹 “ (𝐺‘(◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁)))
22		f1of1 6851	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝑉⟶1-1onto𝑊 → 𝐹:𝑉⟶1-1𝑊)
23	22	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) → 𝐹:𝑉⟶1-1𝑊)
24	23	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) → 𝐹:𝑉⟶1-1𝑊)
25	24	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → 𝐹:𝑉⟶1-1𝑊)
26		simp1lr 1256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → 𝐺:𝐴⟶𝒫 𝑉)
27		simp1r 1217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → (◡𝐼‘𝐽) ∈ 𝐴)
28	26, 27	ffvelcdmd 7115	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → (𝐺‘(◡𝐼‘𝐽)) ∈ 𝒫 𝑉)
29	28	elpwid 4569	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑉)
30		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → 𝑁 ⊆ 𝑉)
31	30	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → 𝑁 ⊆ 𝑉)
32		f1imass 7297	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:𝑉⟶1-1𝑊 ∧ ((𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑉 ∧ 𝑁 ⊆ 𝑉)) → ((𝐹 “ (𝐺‘(◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) ↔ (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))
33	25, 29, 31, 32	syl12anc 850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → ((𝐹 “ (𝐺‘(◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) ↔ (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))
34	33	biimpd 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → ((𝐹 “ (𝐺‘(◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))
35	34	3exp 1137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) → (𝐽 ∈ 𝐵 → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → ((𝐹 “ (𝐺‘(◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))))
36	35	com24 96	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) → ((𝐹 “ (𝐺‘(◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))))
37	36	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽)))) → ((𝐹 “ (𝐺‘(◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))))
38	21, 37	sylbid 243	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽)))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))))
39	38	ex 418	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) → ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁)))))
40	39	com25 100	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) → (𝐽 ∈ 𝐵 → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽))) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁)))))
41	40	imp42 432	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽))) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))
42	19, 41	sylbid 243	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → ((𝐻‘(𝐼‘(◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽))) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))
43	42	ex 418	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → ((𝐻‘(𝐼‘(◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽))) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁)))
44	43	com23 87	. . . . . . . . . . . 12 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝐻‘(𝐼‘(◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽))) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁)))
45	44	ex 418	. . . . . . . . . . 11 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝐻‘(𝐼‘(◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽))) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))))
46	45	com23 87	. . . . . . . . . 10 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) → ((𝐻‘(𝐼‘(◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(◡𝐼‘𝐽))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))))
47	15, 46	syld 48	. . . . . . . . 9 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (◡𝐼‘𝐽) ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))))
48	47	ex 418	. . . . . . . 8 ⊢ ((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) → ((◡𝐼‘𝐽) ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁)))))
49	48	com25 100	. . . . . . 7 ⊢ ((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((◡𝐼‘𝐽) ∈ 𝐴 → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁)))))
50	49	3imp1 1366	. . . . . 6 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((◡𝐼‘𝐽) ∈ 𝐴 → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁))
51	9, 50	mpd 16	. . . . 5 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁)
52	6, 7, 17	syl2an 608	. . . . 5 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (𝐼‘(◡𝐼‘𝐽)) = 𝐽)
53	51, 52	jca 521	. . . 4 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝐺‘(◡𝐼‘𝐽)) ⊆ 𝑁 ∧ (𝐼‘(◡𝐼‘𝐽)) = 𝐽))
54	4, 9, 53	rspcedvdw 3583	. . 3 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽))
55	54	ex 418	. 2 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)))
56		f1of 6852	. . . . . . . 8 ⊢ (𝐼:𝐴⟶1-1onto𝐵 → 𝐼:𝐴⟶𝐵)
57	56	adantl 487	. . . . . . 7 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) → 𝐼:𝐴⟶𝐵)
58	57	3ad2ant2 1152	. . . . . 6 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → 𝐼:𝐴⟶𝐵)
59	58	3ad2ant1 1151	. . . . 5 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → 𝐼:𝐴⟶𝐵)
60		simp2 1155	. . . . 5 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → 𝑘 ∈ 𝐴)
61	59, 60	ffvelcdmd 7115	. . . 4 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐼‘𝑘) ∈ 𝐵)
62		2fveq3 6919	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐻‘(𝐼‘𝑖)) = (𝐻‘(𝐼‘𝑘)))
63		fveq2 6914	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → (𝐺‘𝑖) = (𝐺‘𝑘))
64	63	imaeq2d 6068	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐹 “ (𝐺‘𝑖)) = (𝐹 “ (𝐺‘𝑘)))
65	62, 64	eqeq12d 2779	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → ((𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) ↔ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
66	65	rspcv 3576	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
67	66	adantl 487	. . . . . . . . 9 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) ∧ 𝑘 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
68		simp3 1156	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘)))
69		imass2 6071	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑘) ⊆ 𝑁 → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
70	69	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
71	70	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
72	68, 71	eqsstrd 3947	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))
73	72	3exp 1137	. . . . . . . . . 10 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) ∧ 𝑘 ∈ 𝐴) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → ((𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘)) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
74	73	com23 87	. . . . . . . . 9 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) ∧ 𝑘 ∈ 𝐴) → ((𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘)) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
75	67, 74	syld 48	. . . . . . . 8 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) ∧ 𝑘 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
76	75	ex 418	. . . . . . 7 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → (𝑘 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)))))
77	76	com23 87	. . . . . 6 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵)) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝑘 ∈ 𝐴 → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)))))
78	77	3impia 1135	. . . . 5 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → (𝑘 ∈ 𝐴 → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
79	78	3imp 1128	. . . 4 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))
80		eleq1 2852	. . . . . . 7 ⊢ ((𝐼‘𝑘) = 𝐽 → ((𝐼‘𝑘) ∈ 𝐵 ↔ 𝐽 ∈ 𝐵))
81		fveq2 6914	. . . . . . . 8 ⊢ ((𝐼‘𝑘) = 𝐽 → (𝐻‘(𝐼‘𝑘)) = (𝐻‘𝐽))
82	81	sseq1d 3944	. . . . . . 7 ⊢ ((𝐼‘𝑘) = 𝐽 → ((𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁) ↔ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)))
83	80, 82	anbi12d 644	. . . . . 6 ⊢ ((𝐼‘𝑘) = 𝐽 → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
84	83	adantl 487	. . . . 5 ⊢ (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
85	84	3ad2ant3 1153	. . . 4 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
86	61, 79, 85	mpbi2and 725	. . 3 ⊢ ((((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)))
87	86	rexlimdv3a 3171	. 2 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → (∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
88	55, 87	impbid 215	1 ⊢ (((𝐹:𝑉⟶1-1onto𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴⟶1-1onto𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) ↔ ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090   ⊆ wss 3900  𝒫 cpw 4560  ^◡ccnv 5655   “ cima 5659  ⟶wf 6560  ⟶1-1wf1 6561  ⟶1-1ontowf1o 6563  ‘cfv 6564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-f1 6569  df-fo 6570  df-f1o 6571  df-fv 6572

This theorem is used by:  uhgrimisgrgric  49296