Theorem upixp 33524

Description: Universal property of the indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)

Hypotheses

Ref	Expression
upixp.1	⊢ 𝑋 = X𝑏 ∈ 𝐴 (𝐶‘𝑏)
upixp.2	⊢ 𝑃 = (𝑤 ∈ 𝐴 ↦ (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑤)))

Assertion

Ref	Expression
upixp	⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) → ∃!ℎ(ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ)))

Distinct variable groups:   𝐴,𝑎,𝑏,ℎ,𝑤,𝑥   𝑅,𝑎,𝑏,ℎ,𝑤,𝑥   𝑆,𝑎,𝑏,ℎ,𝑤,𝑥   𝐹,𝑎,𝑏,ℎ,𝑤,𝑥   𝐵,𝑎,𝑏,ℎ,𝑤,𝑥   𝐶,𝑎,𝑏,ℎ,𝑤,𝑥   𝑋,𝑎,ℎ,𝑤,𝑥   𝑃,𝑎,ℎ

Allowed substitution hints:   𝑃(𝑥,𝑤,𝑏)   𝑋(𝑏)

Proof of Theorem upixp

Dummy variables 𝑠 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mptexg 6484	. . 3 ⊢ (𝐵 ∈ 𝑆 → (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))) ∈ V)
2	1	3ad2ant2 1083	. 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) → (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))) ∈ V)
3		ffvelrn 6357	. . . . . . . . . 10 ⊢ (((𝐹‘𝑎):𝐵⟶(𝐶‘𝑎) ∧ 𝑢 ∈ 𝐵) → ((𝐹‘𝑎)‘𝑢) ∈ (𝐶‘𝑎))
4	3	expcom 451	. . . . . . . . 9 ⊢ (𝑢 ∈ 𝐵 → ((𝐹‘𝑎):𝐵⟶(𝐶‘𝑎) → ((𝐹‘𝑎)‘𝑢) ∈ (𝐶‘𝑎)))
5	4	ralimdv 2963	. . . . . . . 8 ⊢ (𝑢 ∈ 𝐵 → (∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎) → ∀𝑎 ∈ 𝐴 ((𝐹‘𝑎)‘𝑢) ∈ (𝐶‘𝑎)))
6	5	impcom 446	. . . . . . 7 ⊢ ((∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎) ∧ 𝑢 ∈ 𝐵) → ∀𝑎 ∈ 𝐴 ((𝐹‘𝑎)‘𝑢) ∈ (𝐶‘𝑎))
7	6	3ad2antl3 1225	. . . . . 6 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑢 ∈ 𝐵) → ∀𝑎 ∈ 𝐴 ((𝐹‘𝑎)‘𝑢) ∈ (𝐶‘𝑎))
8		fveq2 6191	. . . . . . . . 9 ⊢ (𝑎 = 𝑠 → (𝐹‘𝑎) = (𝐹‘𝑠))
9	8	fveq1d 6193	. . . . . . . 8 ⊢ (𝑎 = 𝑠 → ((𝐹‘𝑎)‘𝑢) = ((𝐹‘𝑠)‘𝑢))
10		fveq2 6191	. . . . . . . 8 ⊢ (𝑎 = 𝑠 → (𝐶‘𝑎) = (𝐶‘𝑠))
11	9, 10	eleq12d 2695	. . . . . . 7 ⊢ (𝑎 = 𝑠 → (((𝐹‘𝑎)‘𝑢) ∈ (𝐶‘𝑎) ↔ ((𝐹‘𝑠)‘𝑢) ∈ (𝐶‘𝑠)))
12	11	cbvralv 3171	. . . . . 6 ⊢ (∀𝑎 ∈ 𝐴 ((𝐹‘𝑎)‘𝑢) ∈ (𝐶‘𝑎) ↔ ∀𝑠 ∈ 𝐴 ((𝐹‘𝑠)‘𝑢) ∈ (𝐶‘𝑠))
13	7, 12	sylib 208	. . . . 5 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑢 ∈ 𝐵) → ∀𝑠 ∈ 𝐴 ((𝐹‘𝑠)‘𝑢) ∈ (𝐶‘𝑠))
14		simpl1 1064	. . . . . 6 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑢 ∈ 𝐵) → 𝐴 ∈ 𝑅)
15		mptelixpg 7945	. . . . . 6 ⊢ (𝐴 ∈ 𝑅 → ((𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)) ∈ X𝑠 ∈ 𝐴 (𝐶‘𝑠) ↔ ∀𝑠 ∈ 𝐴 ((𝐹‘𝑠)‘𝑢) ∈ (𝐶‘𝑠)))
16	14, 15	syl 17	. . . . 5 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑢 ∈ 𝐵) → ((𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)) ∈ X𝑠 ∈ 𝐴 (𝐶‘𝑠) ↔ ∀𝑠 ∈ 𝐴 ((𝐹‘𝑠)‘𝑢) ∈ (𝐶‘𝑠)))
17	13, 16	mpbird 247	. . . 4 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑢 ∈ 𝐵) → (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)) ∈ X𝑠 ∈ 𝐴 (𝐶‘𝑠))
18		upixp.1	. . . . 5 ⊢ 𝑋 = X𝑏 ∈ 𝐴 (𝐶‘𝑏)
19		fveq2 6191	. . . . . 6 ⊢ (𝑏 = 𝑠 → (𝐶‘𝑏) = (𝐶‘𝑠))
20	19	cbvixpv 7926	. . . . 5 ⊢ X𝑏 ∈ 𝐴 (𝐶‘𝑏) = X𝑠 ∈ 𝐴 (𝐶‘𝑠)
21	18, 20	eqtri 2644	. . . 4 ⊢ 𝑋 = X𝑠 ∈ 𝐴 (𝐶‘𝑠)
22	17, 21	syl6eleqr 2712	. . 3 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑢 ∈ 𝐵) → (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)) ∈ 𝑋)
23		eqid 2622	. . 3 ⊢ (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))) = (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)))
24	22, 23	fmptd 6385	. 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) → (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))):𝐵⟶𝑋)
25		nfv 1843	. . . 4 ⊢ Ⅎ𝑎 𝐴 ∈ 𝑅
26		nfv 1843	. . . 4 ⊢ Ⅎ𝑎 𝐵 ∈ 𝑆
27		nfra1 2941	. . . 4 ⊢ Ⅎ𝑎∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)
28	25, 26, 27	nf3an 1831	. . 3 ⊢ Ⅎ𝑎(𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎))
29		fveq2 6191	. . . . . . . . 9 ⊢ (𝑠 = 𝑎 → (𝐹‘𝑠) = (𝐹‘𝑎))
30	29	fveq1d 6193	. . . . . . . 8 ⊢ (𝑠 = 𝑎 → ((𝐹‘𝑠)‘𝑢) = ((𝐹‘𝑎)‘𝑢))
31		eqid 2622	. . . . . . . 8 ⊢ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)) = (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))
32		fvex 6201	. . . . . . . 8 ⊢ ((𝐹‘𝑠)‘𝑢) ∈ V
33	30, 31, 32	fvmpt3i 6287	. . . . . . 7 ⊢ (𝑎 ∈ 𝐴 → ((𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))‘𝑎) = ((𝐹‘𝑎)‘𝑢))
34	33	adantl 482	. . . . . 6 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑎 ∈ 𝐴) → ((𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))‘𝑎) = ((𝐹‘𝑎)‘𝑢))
35	34	mpteq2dv 4745	. . . . 5 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑎 ∈ 𝐴) → (𝑢 ∈ 𝐵 ↦ ((𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))‘𝑎)) = (𝑢 ∈ 𝐵 ↦ ((𝐹‘𝑎)‘𝑢)))
36	22	adantlr 751	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑎 ∈ 𝐴) ∧ 𝑢 ∈ 𝐵) → (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)) ∈ 𝑋)
37		eqidd 2623	. . . . . 6 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑎 ∈ 𝐴) → (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))) = (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))))
38		fveq2 6191	. . . . . . . . 9 ⊢ (𝑤 = 𝑎 → (𝑥‘𝑤) = (𝑥‘𝑎))
39	38	mpteq2dv 4745	. . . . . . . 8 ⊢ (𝑤 = 𝑎 → (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑤)) = (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑎)))
40		upixp.2	. . . . . . . 8 ⊢ 𝑃 = (𝑤 ∈ 𝐴 ↦ (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑤)))
41		fvex 6201	. . . . . . . . . . . 12 ⊢ (𝐶‘𝑏) ∈ V
42	41	rgenw 2924	. . . . . . . . . . 11 ⊢ ∀𝑏 ∈ 𝐴 (𝐶‘𝑏) ∈ V
43		ixpexg 7932	. . . . . . . . . . 11 ⊢ (∀𝑏 ∈ 𝐴 (𝐶‘𝑏) ∈ V → X𝑏 ∈ 𝐴 (𝐶‘𝑏) ∈ V)
44	42, 43	ax-mp 5	. . . . . . . . . 10 ⊢ X𝑏 ∈ 𝐴 (𝐶‘𝑏) ∈ V
45	18, 44	eqeltri 2697	. . . . . . . . 9 ⊢ 𝑋 ∈ V
46	45	mptex 6486	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑤)) ∈ V
47	39, 40, 46	fvmpt3i 6287	. . . . . . 7 ⊢ (𝑎 ∈ 𝐴 → (𝑃‘𝑎) = (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑎)))
48	47	adantl 482	. . . . . 6 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑎 ∈ 𝐴) → (𝑃‘𝑎) = (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑎)))
49		fveq1 6190	. . . . . 6 ⊢ (𝑥 = (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)) → (𝑥‘𝑎) = ((𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))‘𝑎))
50	36, 37, 48, 49	fmptco 6396	. . . . 5 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑎 ∈ 𝐴) → ((𝑃‘𝑎) ∘ (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)))) = (𝑢 ∈ 𝐵 ↦ ((𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))‘𝑎)))
51		rsp 2929	. . . . . . . 8 ⊢ (∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎) → (𝑎 ∈ 𝐴 → (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)))
52	51	3ad2ant3 1084	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) → (𝑎 ∈ 𝐴 → (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)))
53	52	imp 445	. . . . . 6 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎))
54	53	feqmptd 6249	. . . . 5 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) = (𝑢 ∈ 𝐵 ↦ ((𝐹‘𝑎)‘𝑢)))
55	35, 50, 54	3eqtr4rd 2667	. . . 4 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ 𝑎 ∈ 𝐴) → (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)))))
56	55	ex 450	. . 3 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) → (𝑎 ∈ 𝐴 → (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))))))
57	28, 56	ralrimi 2957	. 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)))))
58		simprl 794	. . . . . 6 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) → ℎ:𝐵⟶𝑋)
59	58	feqmptd 6249	. . . . 5 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) → ℎ = (𝑢 ∈ 𝐵 ↦ (ℎ‘𝑢)))
60		simplrr 801	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) → ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))
61		fveq2 6191	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑠 → (𝑃‘𝑎) = (𝑃‘𝑠))
62	61	coeq1d 5283	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑠 → ((𝑃‘𝑎) ∘ ℎ) = ((𝑃‘𝑠) ∘ ℎ))
63	8, 62	eqeq12d 2637	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑠 → ((𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ) ↔ (𝐹‘𝑠) = ((𝑃‘𝑠) ∘ ℎ)))
64	63	rspccva 3308	. . . . . . . . . . 11 ⊢ ((∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ) ∧ 𝑠 ∈ 𝐴) → (𝐹‘𝑠) = ((𝑃‘𝑠) ∘ ℎ))
65	60, 64	sylan 488	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑠 ∈ 𝐴) → (𝐹‘𝑠) = ((𝑃‘𝑠) ∘ ℎ))
66	65	fveq1d 6193	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑠 ∈ 𝐴) → ((𝐹‘𝑠)‘𝑢) = (((𝑃‘𝑠) ∘ ℎ)‘𝑢))
67		fvco3 6275	. . . . . . . . . . 11 ⊢ ((ℎ:𝐵⟶𝑋 ∧ 𝑢 ∈ 𝐵) → (((𝑃‘𝑠) ∘ ℎ)‘𝑢) = ((𝑃‘𝑠)‘(ℎ‘𝑢)))
68	58, 67	sylan 488	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) → (((𝑃‘𝑠) ∘ ℎ)‘𝑢) = ((𝑃‘𝑠)‘(ℎ‘𝑢)))
69	68	adantr 481	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑠 ∈ 𝐴) → (((𝑃‘𝑠) ∘ ℎ)‘𝑢) = ((𝑃‘𝑠)‘(ℎ‘𝑢)))
70		fveq2 6191	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑠 → (𝑥‘𝑤) = (𝑥‘𝑠))
71	70	mpteq2dv 4745	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑠 → (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑤)) = (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑠)))
72	71, 40, 46	fvmpt3i 6287	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ 𝐴 → (𝑃‘𝑠) = (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑠)))
73	72	adantl 482	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑠 ∈ 𝐴) → (𝑃‘𝑠) = (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑠)))
74	73	fveq1d 6193	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑠 ∈ 𝐴) → ((𝑃‘𝑠)‘(ℎ‘𝑢)) = ((𝑥 ∈ 𝑋 ↦ (𝑥‘𝑠))‘(ℎ‘𝑢)))
75		ffvelrn 6357	. . . . . . . . . . . . 13 ⊢ ((ℎ:𝐵⟶𝑋 ∧ 𝑢 ∈ 𝐵) → (ℎ‘𝑢) ∈ 𝑋)
76	58, 75	sylan 488	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) → (ℎ‘𝑢) ∈ 𝑋)
77		fveq1 6190	. . . . . . . . . . . . 13 ⊢ (𝑥 = (ℎ‘𝑢) → (𝑥‘𝑠) = ((ℎ‘𝑢)‘𝑠))
78		eqid 2622	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑠)) = (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑠))
79		fvex 6201	. . . . . . . . . . . . 13 ⊢ (𝑥‘𝑠) ∈ V
80	77, 78, 79	fvmpt3i 6287	. . . . . . . . . . . 12 ⊢ ((ℎ‘𝑢) ∈ 𝑋 → ((𝑥 ∈ 𝑋 ↦ (𝑥‘𝑠))‘(ℎ‘𝑢)) = ((ℎ‘𝑢)‘𝑠))
81	76, 80	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) → ((𝑥 ∈ 𝑋 ↦ (𝑥‘𝑠))‘(ℎ‘𝑢)) = ((ℎ‘𝑢)‘𝑠))
82	81	adantr 481	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑠 ∈ 𝐴) → ((𝑥 ∈ 𝑋 ↦ (𝑥‘𝑠))‘(ℎ‘𝑢)) = ((ℎ‘𝑢)‘𝑠))
83	74, 82	eqtrd 2656	. . . . . . . . 9 ⊢ (((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑠 ∈ 𝐴) → ((𝑃‘𝑠)‘(ℎ‘𝑢)) = ((ℎ‘𝑢)‘𝑠))
84	66, 69, 83	3eqtrd 2660	. . . . . . . 8 ⊢ (((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) ∧ 𝑠 ∈ 𝐴) → ((𝐹‘𝑠)‘𝑢) = ((ℎ‘𝑢)‘𝑠))
85	84	mpteq2dva 4744	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) → (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)) = (𝑠 ∈ 𝐴 ↦ ((ℎ‘𝑢)‘𝑠)))
86	76, 18	syl6eleq 2711	. . . . . . . . 9 ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) → (ℎ‘𝑢) ∈ X𝑏 ∈ 𝐴 (𝐶‘𝑏))
87		ixpfn 7914	. . . . . . . . 9 ⊢ ((ℎ‘𝑢) ∈ X𝑏 ∈ 𝐴 (𝐶‘𝑏) → (ℎ‘𝑢) Fn 𝐴)
88	86, 87	syl 17	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) → (ℎ‘𝑢) Fn 𝐴)
89		dffn5 6241	. . . . . . . 8 ⊢ ((ℎ‘𝑢) Fn 𝐴 ↔ (ℎ‘𝑢) = (𝑠 ∈ 𝐴 ↦ ((ℎ‘𝑢)‘𝑠)))
90	88, 89	sylib 208	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) → (ℎ‘𝑢) = (𝑠 ∈ 𝐴 ↦ ((ℎ‘𝑢)‘𝑠)))
91	85, 90	eqtr4d 2659	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) ∧ 𝑢 ∈ 𝐵) → (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)) = (ℎ‘𝑢))
92	91	mpteq2dva 4744	. . . . 5 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) → (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))) = (𝑢 ∈ 𝐵 ↦ (ℎ‘𝑢)))
93	59, 92	eqtr4d 2659	. . . 4 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) ∧ (ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ))) → ℎ = (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))))
94	93	ex 450	. . 3 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) → ((ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ)) → ℎ = (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)))))
95	94	alrimiv 1855	. 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) → ∀ℎ((ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ)) → ℎ = (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)))))
96		feq1 6026	. . . 4 ⊢ (ℎ = (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))) → (ℎ:𝐵⟶𝑋 ↔ (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))):𝐵⟶𝑋))
97		coeq2 5280	. . . . . 6 ⊢ (ℎ = (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))) → ((𝑃‘𝑎) ∘ ℎ) = ((𝑃‘𝑎) ∘ (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)))))
98	97	eqeq2d 2632	. . . . 5 ⊢ (ℎ = (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))) → ((𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ) ↔ (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))))))
99	98	ralbidv 2986	. . . 4 ⊢ (ℎ = (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))) → (∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ) ↔ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))))))
100	96, 99	anbi12d 747	. . 3 ⊢ (ℎ = (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))) → ((ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ)) ↔ ((𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))):𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢)))))))
101	100	eqeu 3377	. 2 ⊢ (((𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))) ∈ V ∧ ((𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))):𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))))) ∧ ∀ℎ((ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ)) → ℎ = (𝑢 ∈ 𝐵 ↦ (𝑠 ∈ 𝐴 ↦ ((𝐹‘𝑠)‘𝑢))))) → ∃!ℎ(ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ)))
102	2, 24, 57, 95, 101	syl121anc 1331	1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎):𝐵⟶(𝐶‘𝑎)) → ∃!ℎ(ℎ:𝐵⟶𝑋 ∧ ∀𝑎 ∈ 𝐴 (𝐹‘𝑎) = ((𝑃‘𝑎) ∘ ℎ)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037  ∀wal 1481   = wceq 1483   ∈ wcel 1990  ∃!weu 2470  ∀wral 2912  Vcvv 3200   ↦ cmpt 4729   ∘ ccom 5118   Fn wfn 5883  ⟶wf 5884  ‘cfv 5888  Xcixp 7908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ixp 7909

This theorem is referenced by: (None)