uhgrimisgrgriclem - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > uhgrimisgrgriclem		Structured version Visualization version GIF version

Theorem uhgrimisgrgriclem 47836

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

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

Distinct variable groups: 𝐴,𝑖,𝑘 𝐵,𝑘 𝑖,𝐹,𝑘 𝑖,𝐺,𝑘 𝑖,𝐻,𝑘 𝑖,𝐼,𝑘 𝑖,𝐽,𝑘 𝑘,𝑁 𝑘,𝑉 𝑘,𝑊 Allowed substitution hints: 𝐵(𝑖) 𝑁(𝑖) 𝑉(𝑖) 𝑊(𝑖)

**Proof of Theorem uhgrimisgrgriclem**
Step	Hyp	Ref	Expression
1		fveq2 6907	. . . . . 6 ⊢ (𝑘 = (^◡𝐼‘𝐽) → (𝐺‘𝑘) = (𝐺‘(^◡𝐼‘𝐽)))
2	1	sseq1d 4027	. . . . 5 ⊢ (𝑘 = (^◡𝐼‘𝐽) → ((𝐺‘𝑘) ⊆ 𝑁 ↔ (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
3		fveqeq2 6916	. . . . 5 ⊢ (𝑘 = (^◡𝐼‘𝐽) → ((𝐼‘𝑘) = 𝐽 ↔ (𝐼‘(^◡𝐼‘𝐽)) = 𝐽))
4	2, 3	anbi12d 632	. . . 4 ⊢ (𝑘 = (^◡𝐼‘𝐽) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ↔ ((𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁 ∧ (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)))
5		simpr 484	. . . . . 6 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → 𝐼:𝐴–1-1-onto→𝐵)
6	5	3ad2ant2 1133	. . . . 5 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → 𝐼:𝐴–1-1-onto→𝐵)
7		simpl 482	. . . . 5 ⊢ ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → 𝐽 ∈ 𝐵)
8		f1ocnvdm 7305	. . . . 5 ⊢ ((𝐼:𝐴–1-1-onto→𝐵 ∧ 𝐽 ∈ 𝐵) → (^◡𝐼‘𝐽) ∈ 𝐴)
9	6, 7, 8	syl2an 596	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (^◡𝐼‘𝐽) ∈ 𝐴)
10		2fveq3 6912	. . . . . . . . . . . . 13 ⊢ (𝑖 = (^◡𝐼‘𝐽) → (𝐻‘(𝐼‘𝑖)) = (𝐻‘(𝐼‘(^◡𝐼‘𝐽))))
11		fveq2 6907	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (^◡𝐼‘𝐽) → (𝐺‘𝑖) = (𝐺‘(^◡𝐼‘𝐽)))
12	11	imaeq2d 6080	. . . . . . . . . . . . 13 ⊢ (𝑖 = (^◡𝐼‘𝐽) → (𝐹 “ (𝐺‘𝑖)) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))))
13	10, 12	eqeq12d 2751	. . . . . . . . . . . 12 ⊢ (𝑖 = (^◡𝐼‘𝐽) → ((𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) ↔ (𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
14	13	rspcv 3618	. . . . . . . . . . 11 ⊢ ((^◡𝐼‘𝐽) ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
15	14	adantl 481	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
16	7	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → 𝐽 ∈ 𝐵)
17		f1ocnvfv2 7297	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼:𝐴–1-1-onto→𝐵 ∧ 𝐽 ∈ 𝐵) → (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)
18	5, 16, 17	syl2anr 597	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)
19	18	fveqeq2d 6915	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ↔ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
20		sseq1 4021	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) ↔ (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁)))
21	20	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) ↔ (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁)))
22		f1of1 6848	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–1-1→𝑊)
23	22	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) → 𝐹:𝑉–1-1→𝑊)
24	23	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → 𝐹:𝑉–1-1→𝑊)
25	24	3ad2ant1 1132	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → 𝐹:𝑉–1-1→𝑊)
26		simp1lr 1236	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → 𝐺:𝐴⟶𝒫 𝑉)
27		simp1r 1197	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (^◡𝐼‘𝐽) ∈ 𝐴)
28	26, 27	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝐺‘(^◡𝐼‘𝐽)) ∈ 𝒫 𝑉)
29	28	elpwid 4614	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑉)
30		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → 𝑁 ⊆ 𝑉)
31	30	3ad2ant3 1134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → 𝑁 ⊆ 𝑉)
32		f1imass 7284	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:𝑉–1-1→𝑊 ∧ ((𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑉 ∧ 𝑁 ⊆ 𝑉)) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) ↔ (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
33	25, 29, 31, 32	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) ↔ (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
34	33	biimpd 229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
35	34	3exp 1118	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → (𝐽 ∈ 𝐵 → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
36	35	com24 95	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
37	36	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
38	21, 37	sylbid 240	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
39	38	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))))
40	39	com25 99	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → (𝐽 ∈ 𝐵 → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))))
41	40	imp42 426	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
42	19, 41	sylbid 240	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
43	42	ex 412	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))
44	43	com23 86	. . . . . . . . . . . 12 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))
45	44	ex 412	. . . . . . . . . . 11 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
46	45	com23 86	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
47	15, 46	syld 47	. . . . . . . . 9 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
48	47	ex 412	. . . . . . . 8 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) → ((^◡𝐼‘𝐽) ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))))
49	48	com25 99	. . . . . . 7 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((^◡𝐼‘𝐽) ∈ 𝐴 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))))
50	49	3imp1 1346	. . . . . 6 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((^◡𝐼‘𝐽) ∈ 𝐴 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
51	9, 50	mpd 15	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)
52	6, 7, 17	syl2an 596	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)
53	51, 52	jca 511	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁 ∧ (𝐼‘(^◡𝐼‘𝐽)) = 𝐽))
54	4, 9, 53	rspcedvdw 3625	. . 3 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽))
55	54	ex 412	. 2 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)))
56		f1of 6849	. . . . . . . 8 ⊢ (𝐼:𝐴–1-1-onto→𝐵 → 𝐼:𝐴⟶𝐵)
57	56	adantl 481	. . . . . . 7 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → 𝐼:𝐴⟶𝐵)
58	57	3ad2ant2 1133	. . . . . 6 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → 𝐼:𝐴⟶𝐵)
59	58	3ad2ant1 1132	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → 𝐼:𝐴⟶𝐵)
60		simp2 1136	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → 𝑘 ∈ 𝐴)
61	59, 60	ffvelcdmd 7105	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐼‘𝑘) ∈ 𝐵)
62		2fveq3 6912	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐻‘(𝐼‘𝑖)) = (𝐻‘(𝐼‘𝑘)))
63		fveq2 6907	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → (𝐺‘𝑖) = (𝐺‘𝑘))
64	63	imaeq2d 6080	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐹 “ (𝐺‘𝑖)) = (𝐹 “ (𝐺‘𝑘)))
65	62, 64	eqeq12d 2751	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → ((𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) ↔ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
66	65	rspcv 3618	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
67	66	adantl 481	. . . . . . . . 9 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
68		simp3 1137	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘)))
69		imass2 6123	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑘) ⊆ 𝑁 → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
70	69	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
71	70	3ad2ant2 1133	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
72	68, 71	eqsstrd 4034	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))
73	72	3exp 1118	. . . . . . . . . 10 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → ((𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘)) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
74	73	com23 86	. . . . . . . . 9 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) → ((𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘)) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
75	67, 74	syld 47	. . . . . . . 8 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
76	75	ex 412	. . . . . . 7 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝑘 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)))))
77	76	com23 86	. . . . . 6 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝑘 ∈ 𝐴 → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)))))
78	77	3impia 1116	. . . . 5 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → (𝑘 ∈ 𝐴 → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
79	78	3imp 1110	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))
80		eleq1 2827	. . . . . . 7 ⊢ ((𝐼‘𝑘) = 𝐽 → ((𝐼‘𝑘) ∈ 𝐵 ↔ 𝐽 ∈ 𝐵))
81		fveq2 6907	. . . . . . . 8 ⊢ ((𝐼‘𝑘) = 𝐽 → (𝐻‘(𝐼‘𝑘)) = (𝐻‘𝐽))
82	81	sseq1d 4027	. . . . . . 7 ⊢ ((𝐼‘𝑘) = 𝐽 → ((𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁) ↔ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)))
83	80, 82	anbi12d 632	. . . . . 6 ⊢ ((𝐼‘𝑘) = 𝐽 → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
84	83	adantl 481	. . . . 5 ⊢ (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
85	84	3ad2ant3 1134	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
86	61, 79, 85	mpbi2and 712	. . 3 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)))
87	86	rexlimdv3a 3157	. 2 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → (∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
88	55, 87	impbid 212	1 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) ↔ ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 ∀wral 3059 ∃wrex 3068 ⊆ wss 3963 𝒫 cpw 4605 ^◡ccnv 5688 “ cima 5692 ⟶wf 6559 –1-1→wf1 6560 –1-1-onto→wf1o 6562 ‘cfv 6563

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-br 5149 df-opab 5211 df-id 5583 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571

This theorem is referenced by: uhgrimisgrgric 47837

W3C validator