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 48678

Description: Lemma for uhgrimisgrgric 48679. (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 6883	. . . . . 6 ⊢ (𝑘 = (^◡𝐼‘𝐽) → (𝐺‘𝑘) = (𝐺‘(^◡𝐼‘𝐽)))
2	1	sseq1d 3969	. . . . 5 ⊢ (𝑘 = (^◡𝐼‘𝐽) → ((𝐺‘𝑘) ⊆ 𝑁 ↔ (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
3		fveqeq2 6892	. . . . 5 ⊢ (𝑘 = (^◡𝐼‘𝐽) → ((𝐼‘𝑘) = 𝐽 ↔ (𝐼‘(^◡𝐼‘𝐽)) = 𝐽))
4	2, 3	anbi12d 643	. . . 4 ⊢ (𝑘 = (^◡𝐼‘𝐽) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ↔ ((𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁 ∧ (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)))
5		simpr 489	. . . . . 6 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → 𝐼:𝐴–1-1-onto→𝐵)
6	5	3ad2ant2 1152	. . . . 5 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → 𝐼:𝐴–1-1-onto→𝐵)
7		simpl 487	. . . . 5 ⊢ ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → 𝐽 ∈ 𝐵)
8		f1ocnvdm 7285	. . . . 5 ⊢ ((𝐼:𝐴–1-1-onto→𝐵 ∧ 𝐽 ∈ 𝐵) → (^◡𝐼‘𝐽) ∈ 𝐴)
9	6, 7, 8	syl2an 607	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (^◡𝐼‘𝐽) ∈ 𝐴)
10		2fveq3 6888	. . . . . . . . . . . . 13 ⊢ (𝑖 = (^◡𝐼‘𝐽) → (𝐻‘(𝐼‘𝑖)) = (𝐻‘(𝐼‘(^◡𝐼‘𝐽))))
11		fveq2 6883	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (^◡𝐼‘𝐽) → (𝐺‘𝑖) = (𝐺‘(^◡𝐼‘𝐽)))
12	11	imaeq2d 6064	. . . . . . . . . . . . 13 ⊢ (𝑖 = (^◡𝐼‘𝐽) → (𝐹 “ (𝐺‘𝑖)) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))))
13	10, 12	eqeq12d 2779	. . . . . . . . . . . 12 ⊢ (𝑖 = (^◡𝐼‘𝐽) → ((𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) ↔ (𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
14	13	rspcv 3578	. . . . . . . . . . 11 ⊢ ((^◡𝐼‘𝐽) ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
15	14	adantl 486	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
16	7	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → 𝐽 ∈ 𝐵)
17		f1ocnvfv2 7277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐼:𝐴–1-1-onto→𝐵 ∧ 𝐽 ∈ 𝐵) → (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)
18	5, 16, 17	syl2anr 608	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)
19	18	fveqeq2d 6891	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ↔ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))))
20		sseq1 3963	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) ↔ (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁)))
21	20	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) ↔ (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁)))
22		f1of1 6821	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹:𝑉–1-1-onto→𝑊 → 𝐹:𝑉–1-1→𝑊)
23	22	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) → 𝐹:𝑉–1-1→𝑊)
24	23	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → 𝐹:𝑉–1-1→𝑊)
25	24	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → 𝐹:𝑉–1-1→𝑊)
26		simp1lr 1256	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → 𝐺:𝐴⟶𝒫 𝑉)
27		simp1r 1217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (^◡𝐼‘𝐽) ∈ 𝐴)
28	26, 27	ffvelcdmd 7082	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝐺‘(^◡𝐼‘𝐽)) ∈ 𝒫 𝑉)
29	28	elpwid 4572	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑉)
30		simpl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → 𝑁 ⊆ 𝑉)
31	30	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → 𝑁 ⊆ 𝑉)
32		f1imass 7264	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹:𝑉–1-1→𝑊 ∧ ((𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑉 ∧ 𝑁 ⊆ 𝑉)) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) ↔ (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
33	25, 29, 31, 32	syl12anc 849	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) ↔ (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
34	33	biimpd 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ 𝐽 ∈ 𝐵 ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
35	34	3exp 1137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → (𝐽 ∈ 𝐵 → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
36	35	com24 96	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
37	36	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))) → ((𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
38	21, 37	sylbid 243	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽)))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
39	38	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐽 ∈ 𝐵 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))))
40	39	com25 100	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → (𝐽 ∈ 𝐵 → ((𝐻‘𝐽) ⊆ (𝐹 “ 𝑁) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))))
41	40	imp42 431	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐻‘𝐽) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
42	19, 41	sylbid 243	. . . . . . . . . . . . . 14 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
43	42	ex 417	. . . . . . . . . . . . 13 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))
44	43	com23 87	. . . . . . . . . . . 12 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))
45	44	ex 417	. . . . . . . . . . 11 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
46	45	com23 87	. . . . . . . . . 10 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → ((𝐻‘(𝐼‘(^◡𝐼‘𝐽))) = (𝐹 “ (𝐺‘(^◡𝐼‘𝐽))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
47	15, 46	syld 48	. . . . . . . . 9 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (^◡𝐼‘𝐽) ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))))
48	47	ex 417	. . . . . . . 8 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) → ((^◡𝐼‘𝐽) ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))))
49	48	com25 100	. . . . . . 7 ⊢ ((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) → ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ((^◡𝐼‘𝐽) ∈ 𝐴 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)))))
50	49	3imp1 1366	. . . . . 6 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((^◡𝐼‘𝐽) ∈ 𝐴 → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁))
51	9, 50	mpd 16	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁)
52	6, 7, 17	syl2an 607	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → (𝐼‘(^◡𝐼‘𝐽)) = 𝐽)
53	51, 52	jca 520	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ((𝐺‘(^◡𝐼‘𝐽)) ⊆ 𝑁 ∧ (𝐼‘(^◡𝐼‘𝐽)) = 𝐽))
54	4, 9, 53	rspcedvdw 3585	. . 3 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))) → ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽))
55	54	ex 417	. 2 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) → ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)))
56		f1of 6822	. . . . . . . 8 ⊢ (𝐼:𝐴–1-1-onto→𝐵 → 𝐼:𝐴⟶𝐵)
57	56	adantl 486	. . . . . . 7 ⊢ ((𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) → 𝐼:𝐴⟶𝐵)
58	57	3ad2ant2 1152	. . . . . 6 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → 𝐼:𝐴⟶𝐵)
59	58	3ad2ant1 1151	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → 𝐼:𝐴⟶𝐵)
60		simp2 1155	. . . . 5 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → 𝑘 ∈ 𝐴)
61	59, 60	ffvelcdmd 7082	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐼‘𝑘) ∈ 𝐵)
62		2fveq3 6888	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐻‘(𝐼‘𝑖)) = (𝐻‘(𝐼‘𝑘)))
63		fveq2 6883	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑘 → (𝐺‘𝑖) = (𝐺‘𝑘))
64	63	imaeq2d 6064	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝐹 “ (𝐺‘𝑖)) = (𝐹 “ (𝐺‘𝑘)))
65	62, 64	eqeq12d 2779	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → ((𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) ↔ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
66	65	rspcv 3578	. . . . . . . . . 10 ⊢ (𝑘 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
67	66	adantl 486	. . . . . . . . 9 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))))
68		simp3 1156	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘)))
69		imass2 6106	. . . . . . . . . . . . . 14 ⊢ ((𝐺‘𝑘) ⊆ 𝑁 → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
70	69	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
71	70	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐹 “ (𝐺‘𝑘)) ⊆ (𝐹 “ 𝑁))
72	68, 71	eqsstrd 3972	. . . . . . . . . . 11 ⊢ (((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) ∧ (𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘))) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))
73	72	3exp 1137	. . . . . . . . . 10 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → ((𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘)) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
74	73	com23 87	. . . . . . . . 9 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) → ((𝐻‘(𝐼‘𝑘)) = (𝐹 “ (𝐺‘𝑘)) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
75	67, 74	syld 48	. . . . . . . 8 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) ∧ 𝑘 ∈ 𝐴) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
76	75	ex 417	. . . . . . 7 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (𝑘 ∈ 𝐴 → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)))))
77	76	com23 87	. . . . . 6 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵)) → (∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖)) → (𝑘 ∈ 𝐴 → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)))))
78	77	3impia 1135	. . . . 5 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → (𝑘 ∈ 𝐴 → (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))))
79	78	3imp 1128	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁))
80		eleq1 2851	. . . . . . 7 ⊢ ((𝐼‘𝑘) = 𝐽 → ((𝐼‘𝑘) ∈ 𝐵 ↔ 𝐽 ∈ 𝐵))
81		fveq2 6883	. . . . . . . 8 ⊢ ((𝐼‘𝑘) = 𝐽 → (𝐻‘(𝐼‘𝑘)) = (𝐻‘𝐽))
82	81	sseq1d 3969	. . . . . . 7 ⊢ ((𝐼‘𝑘) = 𝐽 → ((𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁) ↔ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)))
83	80, 82	anbi12d 643	. . . . . 6 ⊢ ((𝐼‘𝑘) = 𝐽 → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
84	83	adantl 486	. . . . 5 ⊢ (((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
85	84	3ad2ant3 1153	. . . 4 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (((𝐼‘𝑘) ∈ 𝐵 ∧ (𝐻‘(𝐼‘𝑘)) ⊆ (𝐹 “ 𝑁)) ↔ (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
86	61, 79, 85	mpbi2and 724	. . 3 ⊢ ((((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) ∧ 𝑘 ∈ 𝐴 ∧ ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)) → (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)))
87	86	rexlimdv3a 3170	. 2 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → (∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽) → (𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁))))
88	55, 87	impbid 215	1 ⊢ (((𝐹:𝑉–1-1-onto→𝑊 ∧ 𝐺:𝐴⟶𝒫 𝑉) ∧ (𝑁 ⊆ 𝑉 ∧ 𝐼:𝐴–1-1-onto→𝐵) ∧ ∀𝑖 ∈ 𝐴 (𝐻‘(𝐼‘𝑖)) = (𝐹 “ (𝐺‘𝑖))) → ((𝐽 ∈ 𝐵 ∧ (𝐻‘𝐽) ⊆ (𝐹 “ 𝑁)) ↔ ∃𝑘 ∈ 𝐴 ((𝐺‘𝑘) ⊆ 𝑁 ∧ (𝐼‘𝑘) = 𝐽)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ∀wral 3079 ∃wrex 3089 ⊆ wss 3906 𝒫 cpw 4563 ^◡ccnv 5662 “ cima 5666 ⟶wf 6534 –1-1→wf1 6535 –1-1-onto→wf1o 6537 ‘cfv 6538

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5258 ax-nul 5270 ax-pr 5406

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-ne 2959 df-ral 3080 df-rex 3090 df-rab 3417 df-v 3457 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-br 5111 df-opab 5175 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546

This theorem is referenced by: uhgrimisgrgric 48679

W3C validator