ptpjpre1

Description: The preimage of a projection function can be expressed as an indexed cartesian product. (Contributed by Mario Carneiro, 6-Feb-2015)

		Ref	Expression
	Hypothesis	ptpjpre1.1	$⊢ X = \underset{k \in A}{⨉} ⋃ F (k)$
	Assertion	ptpjpre1	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to {(w \in X ⟼ w (I))}^{-1} [U] = \underset{k \in A}{⨉} if (k = I, U, ⋃ F (k))$

Proof

Step	Hyp	Ref	Expression
1		ptpjpre1.1	$⊢ X = \underset{k \in A}{⨉} ⋃ F (k)$
2		fveq2	$⊢ k = I \to w (k) = w (I)$
3		fveq2	$⊢ k = I \to F (k) = F (I)$
4	3	unieqd	$⊢ k = I \to ⋃ F (k) = ⋃ F (I)$
5	2 4	eleq12d	$⊢ k = I \to (w (k) \in ⋃ F (k) \leftrightarrow w (I) \in ⋃ F (I))$
6		vex	$⊢ w \in V$
7	6	elixp	$⊢ w \in \underset{k \in A}{⨉} ⋃ F (k) \leftrightarrow (w Fn A \land \forall k \in A w (k) \in ⋃ F (k))$
8	7	simprbi	$⊢ w \in \underset{k \in A}{⨉} ⋃ F (k) \to \forall k \in A w (k) \in ⋃ F (k)$
9	8 1	eleq2s	$⊢ w \in X \to \forall k \in A w (k) \in ⋃ F (k)$
10	9	adantl	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land w \in X) \to \forall k \in A w (k) \in ⋃ F (k)$
11		simplrl	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land w \in X) \to I \in A$
12	5 10 11	rspcdva	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land w \in X) \to w (I) \in ⋃ F (I)$
13	12	fmpttd	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to (w \in X ⟼ w (I)) : X ⟶ ⋃ F (I)$
14		ffn	$⊢ (w \in X ⟼ w (I)) : X ⟶ ⋃ F (I) \to (w \in X ⟼ w (I)) Fn X$
15		elpreima	$⊢ (w \in X ⟼ w (I)) Fn X \to (z \in {(w \in X ⟼ w (I))}^{-1} [U] \leftrightarrow (z \in X \land (w \in X ⟼ w (I)) (z) \in U))$
16	13 14 15	3syl	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to (z \in {(w \in X ⟼ w (I))}^{-1} [U] \leftrightarrow (z \in X \land (w \in X ⟼ w (I)) (z) \in U))$
17		fveq1	$⊢ w = z \to w (I) = z (I)$
18		eqid	$⊢ (w \in X ⟼ w (I)) = (w \in X ⟼ w (I))$
19		fvex	$⊢ z (I) \in V$
20	17 18 19	fvmpt	$⊢ z \in X \to (w \in X ⟼ w (I)) (z) = z (I)$
21	20	eleq1d	$⊢ z \in X \to ((w \in X ⟼ w (I)) (z) \in U \leftrightarrow z (I) \in U)$
22	21	pm5.32i	$⊢ (z \in X \land (w \in X ⟼ w (I)) (z) \in U) \leftrightarrow (z \in X \land z (I) \in U)$
23	1	eleq2i	$⊢ z \in X \leftrightarrow z \in \underset{k \in A}{⨉} ⋃ F (k)$
24		vex	$⊢ z \in V$
25	24	elixp	$⊢ z \in \underset{k \in A}{⨉} ⋃ F (k) \leftrightarrow (z Fn A \land \forall k \in A z (k) \in ⋃ F (k))$
26	23 25	bitri	$⊢ z \in X \leftrightarrow (z Fn A \land \forall k \in A z (k) \in ⋃ F (k))$
27	26	anbi1i	$⊢ (z \in X \land z (I) \in U) \leftrightarrow ((z Fn A \land \forall k \in A z (k) \in ⋃ F (k)) \land z (I) \in U)$
28		anass	$⊢ ((z Fn A \land \forall k \in A z (k) \in ⋃ F (k)) \land z (I) \in U) \leftrightarrow (z Fn A \land (\forall k \in A z (k) \in ⋃ F (k) \land z (I) \in U))$
29	27 28	bitri	$⊢ (z \in X \land z (I) \in U) \leftrightarrow (z Fn A \land (\forall k \in A z (k) \in ⋃ F (k) \land z (I) \in U))$
30	22 29	bitri	$⊢ (z \in X \land (w \in X ⟼ w (I)) (z) \in U) \leftrightarrow (z Fn A \land (\forall k \in A z (k) \in ⋃ F (k) \land z (I) \in U))$
31		simprl	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land (z (I) \in U \land z (k) \in ⋃ F (k))) \to z (I) \in U$
32		fveq2	$⊢ k = I \to z (k) = z (I)$
33		iftrue	$⊢ k = I \to if (k = I, U, ⋃ F (k)) = U$
34	32 33	eleq12d	$⊢ k = I \to (z (k) \in if (k = I, U, ⋃ F (k)) \leftrightarrow z (I) \in U)$
35	31 34	syl5ibrcom	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land (z (I) \in U \land z (k) \in ⋃ F (k))) \to (k = I \to z (k) \in if (k = I, U, ⋃ F (k)))$
36		simprr	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land (z (I) \in U \land z (k) \in ⋃ F (k))) \to z (k) \in ⋃ F (k)$
37		iffalse	$⊢ \neg k = I \to if (k = I, U, ⋃ F (k)) = ⋃ F (k)$
38	37	eleq2d	$⊢ \neg k = I \to (z (k) \in if (k = I, U, ⋃ F (k)) \leftrightarrow z (k) \in ⋃ F (k))$
39	36 38	syl5ibrcom	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land (z (I) \in U \land z (k) \in ⋃ F (k))) \to (\neg k = I \to z (k) \in if (k = I, U, ⋃ F (k)))$
40	35 39	pm2.61d	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land (z (I) \in U \land z (k) \in ⋃ F (k))) \to z (k) \in if (k = I, U, ⋃ F (k))$
41	40	expr	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land z (I) \in U) \to (z (k) \in ⋃ F (k) \to z (k) \in if (k = I, U, ⋃ F (k)))$
42	41	ralimdv	$⊢ (((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \land z (I) \in U) \to (\forall k \in A z (k) \in ⋃ F (k) \to \forall k \in A z (k) \in if (k = I, U, ⋃ F (k)))$
43	42	expimpd	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to ((z (I) \in U \land \forall k \in A z (k) \in ⋃ F (k)) \to \forall k \in A z (k) \in if (k = I, U, ⋃ F (k)))$
44	43	ancomsd	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to ((\forall k \in A z (k) \in ⋃ F (k) \land z (I) \in U) \to \forall k \in A z (k) \in if (k = I, U, ⋃ F (k)))$
45		elssuni	$⊢ U \in F (I) \to U \subseteq ⋃ F (I)$
46	45	ad2antll	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to U \subseteq ⋃ F (I)$
47	33 4	sseq12d	$⊢ k = I \to (if (k = I, U, ⋃ F (k)) \subseteq ⋃ F (k) \leftrightarrow U \subseteq ⋃ F (I))$
48	46 47	syl5ibrcom	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to (k = I \to if (k = I, U, ⋃ F (k)) \subseteq ⋃ F (k))$
49		ssid	$⊢ ⋃ F (k) \subseteq ⋃ F (k)$
50	37 49	eqsstrdi	$⊢ \neg k = I \to if (k = I, U, ⋃ F (k)) \subseteq ⋃ F (k)$
51	48 50	pm2.61d1	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to if (k = I, U, ⋃ F (k)) \subseteq ⋃ F (k)$
52	51	sseld	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to (z (k) \in if (k = I, U, ⋃ F (k)) \to z (k) \in ⋃ F (k))$
53	52	ralimdv	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to (\forall k \in A z (k) \in if (k = I, U, ⋃ F (k)) \to \forall k \in A z (k) \in ⋃ F (k))$
54	34	rspcv	$⊢ I \in A \to (\forall k \in A z (k) \in if (k = I, U, ⋃ F (k)) \to z (I) \in U)$
55	54	ad2antrl	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to (\forall k \in A z (k) \in if (k = I, U, ⋃ F (k)) \to z (I) \in U)$
56	53 55	jcad	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to (\forall k \in A z (k) \in if (k = I, U, ⋃ F (k)) \to (\forall k \in A z (k) \in ⋃ F (k) \land z (I) \in U))$
57	44 56	impbid	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to ((\forall k \in A z (k) \in ⋃ F (k) \land z (I) \in U) \leftrightarrow \forall k \in A z (k) \in if (k = I, U, ⋃ F (k)))$
58	57	anbi2d	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to ((z Fn A \land (\forall k \in A z (k) \in ⋃ F (k) \land z (I) \in U)) \leftrightarrow (z Fn A \land \forall k \in A z (k) \in if (k = I, U, ⋃ F (k))))$
59	30 58	syl5bb	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to ((z \in X \land (w \in X ⟼ w (I)) (z) \in U) \leftrightarrow (z Fn A \land \forall k \in A z (k) \in if (k = I, U, ⋃ F (k))))$
60	16 59	bitrd	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to (z \in {(w \in X ⟼ w (I))}^{-1} [U] \leftrightarrow (z Fn A \land \forall k \in A z (k) \in if (k = I, U, ⋃ F (k))))$
61	24	elixp	$⊢ z \in \underset{k \in A}{⨉} if (k = I, U, ⋃ F (k)) \leftrightarrow (z Fn A \land \forall k \in A z (k) \in if (k = I, U, ⋃ F (k)))$
62	60 61	bitr4di	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to (z \in {(w \in X ⟼ w (I))}^{-1} [U] \leftrightarrow z \in \underset{k \in A}{⨉} if (k = I, U, ⋃ F (k)))$
63	62	eqrdv	$⊢ ((A \in V \land F : A ⟶ Top) \land (I \in A \land U \in F (I))) \to {(w \in X ⟼ w (I))}^{-1} [U] = \underset{k \in A}{⨉} if (k = I, U, ⋃ F (k))$

Metamath Proof Explorer

Theorem ptpjpre1

Proof