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 48421

Description: Lemma for uhgrimisgrgric 48422. (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 6827	. . . . . 6 ⊢ (𝑘 = (^◡𝐼‘𝐽) → (𝐺‘𝑘) = (𝐺‘(^◡𝐼‘𝐽)))
2	1	sseq1d 3946	. . . . 5 ⊢ (𝑘 = (^◡𝐼‘𝐽) → ((𝐺‘𝑘) ⊆ 𝑁 ↔ (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
3		fveqeq2 6836	. . . . 5 ⊢ (𝑘 = (^◡𝐼‘𝐽) → ((𝐼‘𝑘) = 𝐽 ↔ (𝐼‘(^◡𝐼‘𝐽)) = 𝐽))
4	2, 3	anbi12d 638	. . . 4 ⊢ (𝑘 = (^◡𝐼‘𝐽) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ↔ ((𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁 ∧ (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)))
5		simpr 485	. . . . . 6 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → 𝐼:𝐴–1-1-onto→𝐵)
6	5	3ad2ant2 1140	. . . . 5 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → 𝐼:𝐴–1-1-onto→𝐵)
7		simpl 483	. . . . 5 ⊢ ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → 𝐽 ∈ 𝐵)
8		f1ocnvdm 7229	. . . . 5 ⊢ ((𝐼:𝐴–1-1-onto→𝐵 ∧ 𝐽 ∈ 𝐵) → (^◡𝐼‘𝐽) ∈ 𝐴)
9	6, 7, 8	syl2an 602	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (^◡𝐼‘𝐽) ∈ 𝐴)
10		2fveq3 6832	. . . . . . . . . . . . 13 ⊢ (𝑖 = (^◡𝐼‘𝐽) → (𝐻‘(𝐼‘𝑖)) = (𝐻‘(𝐼‘(^◡𝐼‘𝐽))))
11		fveq2 6827	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (^◡𝐼‘𝐽) → (𝐺‘𝑖) = (𝐺‘(^◡𝐼‘𝐽)))
12	11	imaeq2d 6012	. . . . . . . . . . . . 13 ⊢ (𝑖 = (^◡𝐼‘𝐽) → (𝐹 “ (𝐺‘𝑖)) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))))
13	10, 12	eqeq12d 2755	. . . . . . . . . . . 12 ⊢ (𝑖 = (^◡𝐼‘𝐽) → ((𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) ↔ (𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
14	13	rspcv 3556	. . . . . . . . . . 11 ⊢ ((^◡𝐼‘𝐽) ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
15	14	adantl 482	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
16	7	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → 𝐽 ∈ 𝐵)
17		f1ocnvfv2 7221	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼:𝐴–1-1-onto→𝐵 ∧ 𝐽 ∈ 𝐵) → (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)
18	5, 16, 17	syl2anr 603	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)
19	18	fveqeq2d 6835	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ↔ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
20		sseq1 3940	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) ↔ (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁)))
21	20	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) ↔ (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁)))
22		f1of1 6766	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–1-1→𝑊)
23	22	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) → 𝐹:𝑉–1-1→𝑊)
24	23	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → 𝐹:𝑉–1-1→𝑊)
25	24	3ad2ant1 1139	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → 𝐹:𝑉–1-1→𝑊)
26		simp1lr 1244	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → 𝐺:𝐴⟶𝒫 𝑉)
27		simp1r 1205	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (^◡𝐼‘𝐽) ∈ 𝐴)
28	26, 27	ffvelcdmd 7026	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝐺‘(^◡𝐼‘𝐽)) ∈ 𝒫 𝑉)
29	28	elpwid 4538	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑉)
30		simpl 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → 𝑁 ⊆ 𝑉)
31	30	3ad2ant3 1141	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → 𝑁 ⊆ 𝑉)
32		f1imass 7208	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:𝑉–1-1→𝑊 ∧ ((𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑉 ∧ 𝑁 ⊆ 𝑉)) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) ↔ (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
33	25, 29, 31, 32	syl12anc 842	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) ↔ (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
34	33	biimpd 230	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
35	34	3exp 1125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → (𝐽 ∈ 𝐵 → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
36	35	com24 95	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
37	36	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
38	21, 37	sylbid 241	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
39	38	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))))
40	39	com25 99	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → (𝐽 ∈ 𝐵 → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))))
41	40	imp42 427	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
42	19, 41	sylbid 241	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
43	42	ex 413	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))
44	43	com23 86	. . . . . . . . . . . 12 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))
45	44	ex 413	. . . . . . . . . . 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 413	. . . . . . . 8 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) → ((^◡𝐼‘𝐽) ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))))
49	48	com25 99	. . . . . . 7 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((^◡𝐼‘𝐽) ∈ 𝐴 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))))
50	49	3imp1 1354	. . . . . 6 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((^◡𝐼‘𝐽) ∈ 𝐴 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
51	9, 50	mpd 15	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)
52	6, 7, 17	syl2an 602	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)
53	51, 52	jca 516	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁 ∧ (𝐼‘(^◡𝐼‘𝐽)) = 𝐽))
54	4, 9, 53	rspcedvdw 3563	. . 3 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽))
55	54	ex 413	. 2 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)))
56		f1of 6767	. . . . . . . 8 ⊢ (𝐼:𝐴–1-1-onto→𝐵 → 𝐼:𝐴⟶𝐵)
57	56	adantl 482	. . . . . . 7 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → 𝐼:𝐴⟶𝐵)
58	57	3ad2ant2 1140	. . . . . 6 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → 𝐼:𝐴⟶𝐵)
59	58	3ad2ant1 1139	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → 𝐼:𝐴⟶𝐵)
60		simp2 1143	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → 𝑘 ∈ 𝐴)
61	59, 60	ffvelcdmd 7026	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐼‘𝑘) ∈ 𝐵)
62		2fveq3 6832	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐻‘(𝐼‘𝑖)) = (𝐻‘(𝐼‘𝑘)))
63		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → (𝐺‘𝑖) = (𝐺‘𝑘))
64	63	imaeq2d 6012	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐹 “ (𝐺‘𝑖)) = (𝐹 “ (𝐺‘𝑘)))
65	62, 64	eqeq12d 2755	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → ((𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) ↔ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
66	65	rspcv 3556	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
67	66	adantl 482	. . . . . . . . 9 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
68		simp3 1144	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘)))
69		imass2 6054	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑘) ⊆ 𝑁 → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
70	69	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
71	70	3ad2ant2 1140	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
72	68, 71	eqsstrd 3949	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))
73	72	3exp 1125	. . . . . . . . . 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 413	. . . . . . 7 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝑘 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)))))
77	76	com23 86	. . . . . 6 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝑘 ∈ 𝐴 → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)))))
78	77	3impia 1123	. . . . 5 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → (𝑘 ∈ 𝐴 → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
79	78	3imp 1116	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))
80		eleq1 2827	. . . . . . 7 ⊢ ((𝐼‘𝑘) = 𝐽 → ((𝐼‘𝑘) ∈ 𝐵 ↔ 𝐽 ∈ 𝐵))
81		fveq2 6827	. . . . . . . 8 ⊢ ((𝐼‘𝑘) = 𝐽 → (𝐻‘(𝐼‘𝑘)) = (𝐻‘𝐽))
82	81	sseq1d 3946	. . . . . . 7 ⊢ ((𝐼‘𝑘) = 𝐽 → ((𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁) ↔ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)))
83	80, 82	anbi12d 638	. . . . . 6 ⊢ ((𝐼‘𝑘) = 𝐽 → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
84	83	adantl 482	. . . . 5 ⊢ (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
85	84	3ad2ant3 1141	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
86	61, 79, 85	mpbi2and 718	. . 3 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)))
87	86	rexlimdv3a 3144	. 2 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → (∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
88	55, 87	impbid 213	1 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) ↔ ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ∀wral 3053 ∃wrex 3063 ⊆ wss 3883 𝒫 cpw 4529 ^◡ccnv 5617 “ cima 5621 ⟶wf 6481 –1-1→wf1 6482 –1-1-onto→wf1o 6484 ‘cfv 6485

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-sep 5218 ax-nul 5228 ax-pr 5362

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-ne 2935 df-ral 3054 df-rex 3064 df-rab 3392 df-v 3433 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-br 5073 df-opab 5135 df-id 5513 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493

This theorem is referenced by: uhgrimisgrgric 48422

W3C validator