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 47782

Description: Lemma for uhgrimisgrgric 47783. (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 6920	. . . . . 6 ⊢ (𝑘 = (^◡𝐼‘𝐽) → (𝐺‘𝑘) = (𝐺‘(^◡𝐼‘𝐽)))
2	1	sseq1d 4040	. . . . 5 ⊢ (𝑘 = (^◡𝐼‘𝐽) → ((𝐺‘𝑘) ⊆ 𝑁 ↔ (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
3		fveqeq2 6929	. . . . 5 ⊢ (𝑘 = (^◡𝐼‘𝐽) → ((𝐼‘𝑘) = 𝐽 ↔ (𝐼‘(^◡𝐼‘𝐽)) = 𝐽))
4	2, 3	anbi12d 631	. . . 4 ⊢ (𝑘 = (^◡𝐼‘𝐽) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ↔ ((𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁 ∧ (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)))
5		simpr 484	. . . . . 6 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → 𝐼:𝐴–1-1-onto→𝐵)
6	5	3ad2ant2 1134	. . . . 5 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → 𝐼:𝐴–1-1-onto→𝐵)
7		simpl 482	. . . . 5 ⊢ ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → 𝐽 ∈ 𝐵)
8		f1ocnvdm 7321	. . . . 5 ⊢ ((𝐼:𝐴–1-1-onto→𝐵 ∧ 𝐽 ∈ 𝐵) → (^◡𝐼‘𝐽) ∈ 𝐴)
9	6, 7, 8	syl2an 595	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (^◡𝐼‘𝐽) ∈ 𝐴)
10		2fveq3 6925	. . . . . . . . . . . . 13 ⊢ (𝑖 = (^◡𝐼‘𝐽) → (𝐻‘(𝐼‘𝑖)) = (𝐻‘(𝐼‘(^◡𝐼‘𝐽))))
11		fveq2 6920	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (^◡𝐼‘𝐽) → (𝐺‘𝑖) = (𝐺‘(^◡𝐼‘𝐽)))
12	11	imaeq2d 6089	. . . . . . . . . . . . 13 ⊢ (𝑖 = (^◡𝐼‘𝐽) → (𝐹 “ (𝐺‘𝑖)) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))))
13	10, 12	eqeq12d 2756	. . . . . . . . . . . 12 ⊢ (𝑖 = (^◡𝐼‘𝐽) → ((𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) ↔ (𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
14	13	rspcv 3631	. . . . . . . . . . 11 ⊢ ((^◡𝐼‘𝐽) ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
15	14	adantl 481	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
16	7	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → 𝐽 ∈ 𝐵)
17		f1ocnvfv2 7313	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼:𝐴–1-1-onto→𝐵 ∧ 𝐽 ∈ 𝐵) → (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)
18	5, 16, 17	syl2anr 596	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)
19	18	fveqeq2d 6928	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ↔ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
20		sseq1 4034	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) ↔ (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁)))
21	20	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) ↔ (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁)))
22		f1of1 6861	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → 𝐹:𝑉–1-1→𝑊)
26		simp1lr 1237	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → 𝐺:𝐴⟶𝒫 𝑉)
27		simp1r 1198	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (^◡𝐼‘𝐽) ∈ 𝐴)
28	26, 27	ffvelcdmd 7119	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝐺‘(^◡𝐼‘𝐽)) ∈ 𝒫 𝑉)
29	28	elpwid 4631	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑉)
30		simpl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → 𝑁 ⊆ 𝑉)
31	30	3ad2ant3 1135	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → 𝑁 ⊆ 𝑉)
32		f1imass 7301	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:𝑉–1-1→𝑊 ∧ ((𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑉 ∧ 𝑁 ⊆ 𝑉)) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) ↔ (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
33	25, 29, 31, 32	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) ↔ (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
34	33	biimpd 229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
35	34	3exp 1119	. . . . . . . . . . . . . . . . . . . . 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 1347	. . . . . 6 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((^◡𝐼‘𝐽) ∈ 𝐴 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
51	9, 50	mpd 15	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)
52	6, 7, 17	syl2an 595	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)
53	51, 52	jca 511	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁 ∧ (𝐼‘(^◡𝐼‘𝐽)) = 𝐽))
54	4, 9, 53	rspcedvdw 3638	. . 3 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽))
55	54	ex 412	. 2 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)))
56		f1of 6862	. . . . . . . 8 ⊢ (𝐼:𝐴–1-1-onto→𝐵 → 𝐼:𝐴⟶𝐵)
57	56	adantl 481	. . . . . . 7 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → 𝐼:𝐴⟶𝐵)
58	57	3ad2ant2 1134	. . . . . 6 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → 𝐼:𝐴⟶𝐵)
59	58	3ad2ant1 1133	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → 𝐼:𝐴⟶𝐵)
60		simp2 1137	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → 𝑘 ∈ 𝐴)
61	59, 60	ffvelcdmd 7119	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐼‘𝑘) ∈ 𝐵)
62		2fveq3 6925	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐻‘(𝐼‘𝑖)) = (𝐻‘(𝐼‘𝑘)))
63		fveq2 6920	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → (𝐺‘𝑖) = (𝐺‘𝑘))
64	63	imaeq2d 6089	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐹 “ (𝐺‘𝑖)) = (𝐹 “ (𝐺‘𝑘)))
65	62, 64	eqeq12d 2756	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → ((𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) ↔ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
66	65	rspcv 3631	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
67	66	adantl 481	. . . . . . . . 9 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
68		simp3 1138	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘)))
69		imass2 6132	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑘) ⊆ 𝑁 → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
70	69	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
71	70	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
72	68, 71	eqsstrd 4047	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))
73	72	3exp 1119	. . . . . . . . . 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 1117	. . . . 5 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → (𝑘 ∈ 𝐴 → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
79	78	3imp 1111	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))
80		eleq1 2832	. . . . . . 7 ⊢ ((𝐼‘𝑘) = 𝐽 → ((𝐼‘𝑘) ∈ 𝐵 ↔ 𝐽 ∈ 𝐵))
81		fveq2 6920	. . . . . . . 8 ⊢ ((𝐼‘𝑘) = 𝐽 → (𝐻‘(𝐼‘𝑘)) = (𝐻‘𝐽))
82	81	sseq1d 4040	. . . . . . 7 ⊢ ((𝐼‘𝑘) = 𝐽 → ((𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁) ↔ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)))
83	80, 82	anbi12d 631	. . . . . 6 ⊢ ((𝐼‘𝑘) = 𝐽 → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
84	83	adantl 481	. . . . 5 ⊢ (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
85	84	3ad2ant3 1135	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
86	61, 79, 85	mpbi2and 711	. . 3 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)))
87	86	rexlimdv3a 3165	. 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 1087 = wceq 1537 ∈ wcel 2108 ∀wral 3067 ∃wrex 3076 ⊆ wss 3976 𝒫 cpw 4622 ^◡ccnv 5699 “ cima 5703 ⟶wf 6569 –1-1→wf1 6570 –1-1-onto→wf1o 6572 ‘cfv 6573

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pr 5447

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-ne 2947 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-br 5167 df-opab 5229 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581

This theorem is referenced by: uhgrimisgrgric 47783

W3C validator