upixp

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

	Ref	Expression
Hypotheses	upixp.1	$⊢ X = \underset{b \in A}{⨉} C (b)$
	upixp.2	$⊢ P = (w \in A ⟼ (x \in X ⟼ x (w)))$
Assertion	upixp	$⊢ (A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \to \exists! h (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)$

Proof

Step	Hyp	Ref	Expression
1		upixp.1	$⊢ X = \underset{b \in A}{⨉} C (b)$
2		upixp.2	$⊢ P = (w \in A ⟼ (x \in X ⟼ x (w)))$
3		mptexg	$⊢ B \in S \to (u \in B ⟼ (s \in A ⟼ F (s) (u))) \in V$
4	3	3ad2ant2	$⊢ (A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \to (u \in B ⟼ (s \in A ⟼ F (s) (u))) \in V$
5		ffvelcdm	$⊢ (F (a) : B ⟶ C (a) \land u \in B) \to F (a) (u) \in C (a)$
6	5	expcom	$⊢ u \in B \to (F (a) : B ⟶ C (a) \to F (a) (u) \in C (a))$
7	6	ralimdv	$⊢ u \in B \to (\forall a \in A F (a) : B ⟶ C (a) \to \forall a \in A F (a) (u) \in C (a))$
8	7	impcom	$⊢ (\forall a \in A F (a) : B ⟶ C (a) \land u \in B) \to \forall a \in A F (a) (u) \in C (a)$
9	8	3ad2antl3	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land u \in B) \to \forall a \in A F (a) (u) \in C (a)$
10		fveq2	$⊢ a = s \to F (a) = F (s)$
11	10	fveq1d	$⊢ a = s \to F (a) (u) = F (s) (u)$
12		fveq2	$⊢ a = s \to C (a) = C (s)$
13	11 12	eleq12d	$⊢ a = s \to (F (a) (u) \in C (a) \leftrightarrow F (s) (u) \in C (s))$
14	13	cbvralvw	$⊢ \forall a \in A F (a) (u) \in C (a) \leftrightarrow \forall s \in A F (s) (u) \in C (s)$
15	9 14	sylib	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land u \in B) \to \forall s \in A F (s) (u) \in C (s)$
16		simpl1	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land u \in B) \to A \in R$
17		mptelixpg	$⊢ A \in R \to ((s \in A ⟼ F (s) (u)) \in \underset{s \in A}{⨉} C (s) \leftrightarrow \forall s \in A F (s) (u) \in C (s))$
18	16 17	syl	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land u \in B) \to ((s \in A ⟼ F (s) (u)) \in \underset{s \in A}{⨉} C (s) \leftrightarrow \forall s \in A F (s) (u) \in C (s))$
19	15 18	mpbird	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land u \in B) \to (s \in A ⟼ F (s) (u)) \in \underset{s \in A}{⨉} C (s)$
20		fveq2	$⊢ b = s \to C (b) = C (s)$
21	20	cbvixpv	$⊢ \underset{b \in A}{⨉} C (b) = \underset{s \in A}{⨉} C (s)$
22	1 21	eqtri	$⊢ X = \underset{s \in A}{⨉} C (s)$
23	19 22	eleqtrrdi	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land u \in B) \to (s \in A ⟼ F (s) (u)) \in X$
24	23	fmpttd	$⊢ (A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \to (u \in B ⟼ (s \in A ⟼ F (s) (u))) : B ⟶ X$
25		nfv	$⊢ Ⅎ a A \in R$
26		nfv	$⊢ Ⅎ a B \in S$
27		nfra1	$⊢ Ⅎ a \forall a \in A F (a) : B ⟶ C (a)$
28	25 26 27	nf3an	$⊢ Ⅎ a (A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a))$
29		fveq2	$⊢ s = a \to F (s) = F (a)$
30	29	fveq1d	$⊢ s = a \to F (s) (u) = F (a) (u)$
31		eqid	$⊢ (s \in A ⟼ F (s) (u)) = (s \in A ⟼ F (s) (u))$
32		fvex	$⊢ F (s) (u) \in V$
33	30 31 32	fvmpt3i	$⊢ a \in A \to (s \in A ⟼ F (s) (u)) (a) = F (a) (u)$
34	33	adantl	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land a \in A) \to (s \in A ⟼ F (s) (u)) (a) = F (a) (u)$
35	34	mpteq2dv	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land a \in A) \to (u \in B ⟼ (s \in A ⟼ F (s) (u)) (a)) = (u \in B ⟼ F (a) (u))$
36	23	adantlr	$⊢ (((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land a \in A) \land u \in B) \to (s \in A ⟼ F (s) (u)) \in X$
37		eqidd	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land a \in A) \to (u \in B ⟼ (s \in A ⟼ F (s) (u))) = (u \in B ⟼ (s \in A ⟼ F (s) (u)))$
38		fveq2	$⊢ w = a \to x (w) = x (a)$
39	38	mpteq2dv	$⊢ w = a \to (x \in X ⟼ x (w)) = (x \in X ⟼ x (a))$
40		fvex	$⊢ C (b) \in V$
41	40	rgenw	$⊢ \forall b \in A C (b) \in V$
42		ixpexg	$⊢ \forall b \in A C (b) \in V \to \underset{b \in A}{⨉} C (b) \in V$
43	41 42	ax-mp	$⊢ \underset{b \in A}{⨉} C (b) \in V$
44	1 43	eqeltri	$⊢ X \in V$
45	44	mptex	$⊢ (x \in X ⟼ x (w)) \in V$
46	39 2 45	fvmpt3i	$⊢ a \in A \to P (a) = (x \in X ⟼ x (a))$
47	46	adantl	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land a \in A) \to P (a) = (x \in X ⟼ x (a))$
48		fveq1	$⊢ x = (s \in A ⟼ F (s) (u)) \to x (a) = (s \in A ⟼ F (s) (u)) (a)$
49	36 37 47 48	fmptco	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land a \in A) \to P (a) \circ (u \in B ⟼ (s \in A ⟼ F (s) (u))) = (u \in B ⟼ (s \in A ⟼ F (s) (u)) (a))$
50		rsp	$⊢ \forall a \in A F (a) : B ⟶ C (a) \to (a \in A \to F (a) : B ⟶ C (a))$
51	50	3ad2ant3	$⊢ (A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \to (a \in A \to F (a) : B ⟶ C (a))$
52	51	imp	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land a \in A) \to F (a) : B ⟶ C (a)$
53	52	feqmptd	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land a \in A) \to F (a) = (u \in B ⟼ F (a) (u))$
54	35 49 53	3eqtr4rd	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land a \in A) \to F (a) = P (a) \circ (u \in B ⟼ (s \in A ⟼ F (s) (u)))$
55	54	ex	$⊢ (A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \to (a \in A \to F (a) = P (a) \circ (u \in B ⟼ (s \in A ⟼ F (s) (u))))$
56	28 55	ralrimi	$⊢ (A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \to \forall a \in A F (a) = P (a) \circ (u \in B ⟼ (s \in A ⟼ F (s) (u)))$
57		simprl	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \to h : B ⟶ X$
58	57	feqmptd	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \to h = (u \in B ⟼ h (u))$
59		simplrr	$⊢ (((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \to \forall a \in A F (a) = P (a) \circ h$
60		fveq2	$⊢ a = s \to P (a) = P (s)$
61	60	coeq1d	$⊢ a = s \to P (a) \circ h = P (s) \circ h$
62	10 61	eqeq12d	$⊢ a = s \to (F (a) = P (a) \circ h \leftrightarrow F (s) = P (s) \circ h)$
63	62	rspccva	$⊢ (\forall a \in A F (a) = P (a) \circ h \land s \in A) \to F (s) = P (s) \circ h$
64	59 63	sylan	$⊢ ((((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \land s \in A) \to F (s) = P (s) \circ h$
65	64	fveq1d	$⊢ ((((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \land s \in A) \to F (s) (u) = (P (s) \circ h) (u)$
66		fvco3	$⊢ (h : B ⟶ X \land u \in B) \to (P (s) \circ h) (u) = P (s) (h (u))$
67	57 66	sylan	$⊢ (((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \to (P (s) \circ h) (u) = P (s) (h (u))$
68	67	adantr	$⊢ ((((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \land s \in A) \to (P (s) \circ h) (u) = P (s) (h (u))$
69		fveq2	$⊢ w = s \to x (w) = x (s)$
70	69	mpteq2dv	$⊢ w = s \to (x \in X ⟼ x (w)) = (x \in X ⟼ x (s))$
71	70 2 45	fvmpt3i	$⊢ s \in A \to P (s) = (x \in X ⟼ x (s))$
72	71	adantl	$⊢ ((((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \land s \in A) \to P (s) = (x \in X ⟼ x (s))$
73	72	fveq1d	$⊢ ((((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \land s \in A) \to P (s) (h (u)) = (x \in X ⟼ x (s)) (h (u))$
74		ffvelcdm	$⊢ (h : B ⟶ X \land u \in B) \to h (u) \in X$
75	57 74	sylan	$⊢ (((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \to h (u) \in X$
76		fveq1	$⊢ x = h (u) \to x (s) = h (u) (s)$
77		eqid	$⊢ (x \in X ⟼ x (s)) = (x \in X ⟼ x (s))$
78		fvex	$⊢ x (s) \in V$
79	76 77 78	fvmpt3i	$⊢ h (u) \in X \to (x \in X ⟼ x (s)) (h (u)) = h (u) (s)$
80	75 79	syl	$⊢ (((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \to (x \in X ⟼ x (s)) (h (u)) = h (u) (s)$
81	80	adantr	$⊢ ((((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \land s \in A) \to (x \in X ⟼ x (s)) (h (u)) = h (u) (s)$
82	73 81	eqtrd	$⊢ ((((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \land s \in A) \to P (s) (h (u)) = h (u) (s)$
83	65 68 82	3eqtrd	$⊢ ((((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \land s \in A) \to F (s) (u) = h (u) (s)$
84	83	mpteq2dva	$⊢ (((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \to (s \in A ⟼ F (s) (u)) = (s \in A ⟼ h (u) (s))$
85	75 1	eleqtrdi	$⊢ (((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \to h (u) \in \underset{b \in A}{⨉} C (b)$
86		ixpfn	$⊢ h (u) \in \underset{b \in A}{⨉} C (b) \to h (u) Fn A$
87	85 86	syl	$⊢ (((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \to h (u) Fn A$
88		dffn5	$⊢ h (u) Fn A \leftrightarrow h (u) = (s \in A ⟼ h (u) (s))$
89	87 88	sylib	$⊢ (((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \to h (u) = (s \in A ⟼ h (u) (s))$
90	84 89	eqtr4d	$⊢ (((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \land u \in B) \to (s \in A ⟼ F (s) (u)) = h (u)$
91	90	mpteq2dva	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \to (u \in B ⟼ (s \in A ⟼ F (s) (u))) = (u \in B ⟼ h (u))$
92	58 91	eqtr4d	$⊢ ((A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \land (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)) \to h = (u \in B ⟼ (s \in A ⟼ F (s) (u)))$
93	92	ex	$⊢ (A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \to ((h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h) \to h = (u \in B ⟼ (s \in A ⟼ F (s) (u))))$
94	93	alrimiv	$⊢ (A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \to \forall h ((h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h) \to h = (u \in B ⟼ (s \in A ⟼ F (s) (u))))$
95		feq1	$⊢ h = (u \in B ⟼ (s \in A ⟼ F (s) (u))) \to (h : B ⟶ X \leftrightarrow (u \in B ⟼ (s \in A ⟼ F (s) (u))) : B ⟶ X)$
96		coeq2	$⊢ h = (u \in B ⟼ (s \in A ⟼ F (s) (u))) \to P (a) \circ h = P (a) \circ (u \in B ⟼ (s \in A ⟼ F (s) (u)))$
97	96	eqeq2d	$⊢ h = (u \in B ⟼ (s \in A ⟼ F (s) (u))) \to (F (a) = P (a) \circ h \leftrightarrow F (a) = P (a) \circ (u \in B ⟼ (s \in A ⟼ F (s) (u))))$
98	97	ralbidv	$⊢ h = (u \in B ⟼ (s \in A ⟼ F (s) (u))) \to (\forall a \in A F (a) = P (a) \circ h \leftrightarrow \forall a \in A F (a) = P (a) \circ (u \in B ⟼ (s \in A ⟼ F (s) (u))))$
99	95 98	anbi12d	$⊢ h = (u \in B ⟼ (s \in A ⟼ F (s) (u))) \to ((h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h) \leftrightarrow ((u \in B ⟼ (s \in A ⟼ F (s) (u))) : B ⟶ X \land \forall a \in A F (a) = P (a) \circ (u \in B ⟼ (s \in A ⟼ F (s) (u)))))$
100	99	eqeu	$⊢ ((u \in B ⟼ (s \in A ⟼ F (s) (u))) \in V \land ((u \in B ⟼ (s \in A ⟼ F (s) (u))) : B ⟶ X \land \forall a \in A F (a) = P (a) \circ (u \in B ⟼ (s \in A ⟼ F (s) (u)))) \land \forall h ((h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h) \to h = (u \in B ⟼ (s \in A ⟼ F (s) (u))))) \to \exists! h (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)$
101	4 24 56 94 100	syl121anc	$⊢ (A \in R \land B \in S \land \forall a \in A F (a) : B ⟶ C (a)) \to \exists! h (h : B ⟶ X \land \forall a \in A F (a) = P (a) \circ h)$

Metamath Proof Explorer

Theorem upixp

Proof