ralxpmap

Description: Quantification over functions in terms of quantification over values and punctured functions. (Contributed by Stefan O'Rear, 27-Feb-2015) (Revised by Stefan O'Rear, 5-May-2015)

		Ref	Expression
	Hypothesis	ralxpmap.j	$⊢ f = g \cup \{⟨J, y⟩\} \to (φ \leftrightarrow ψ)$
	Assertion	ralxpmap	$⊢ J \in T \to (\forall f \in (S^{T}) φ \leftrightarrow \forall y \in S \forall g \in (S^{(T ∖ \{J\})}) ψ)$

Proof

Step	Hyp	Ref	Expression
1		ralxpmap.j	$⊢ f = g \cup \{⟨J, y⟩\} \to (φ \leftrightarrow ψ)$
2		vex	$⊢ g \in V$
3		snex	$⊢ \{⟨J, y⟩\} \in V$
4	2 3	unex	$⊢ g \cup \{⟨J, y⟩\} \in V$
5		simpr	$⊢ (J \in T \land f \in (S^{T})) \to f \in (S^{T})$
6		elmapex	$⊢ f \in (S^{T}) \to (S \in V \land T \in V)$
7	6	adantl	$⊢ (J \in T \land f \in (S^{T})) \to (S \in V \land T \in V)$
8		elmapg	$⊢ (S \in V \land T \in V) \to (f \in (S^{T}) \leftrightarrow f : T ⟶ S)$
9	7 8	syl	$⊢ (J \in T \land f \in (S^{T})) \to (f \in (S^{T}) \leftrightarrow f : T ⟶ S)$
10	5 9	mpbid	$⊢ (J \in T \land f \in (S^{T})) \to f : T ⟶ S$
11		simpl	$⊢ (J \in T \land f \in (S^{T})) \to J \in T$
12	10 11	ffvelrnd	$⊢ (J \in T \land f \in (S^{T})) \to f (J) \in S$
13		difss	$⊢ T ∖ \{J\} \subseteq T$
14		fssres	$⊢ (f : T ⟶ S \land T ∖ \{J\} \subseteq T) \to ({f ↾}_{(T ∖ \{J\})}) : T ∖ \{J\} ⟶ S$
15	10 13 14	sylancl	$⊢ (J \in T \land f \in (S^{T})) \to ({f ↾}_{(T ∖ \{J\})}) : T ∖ \{J\} ⟶ S$
16	6	simpld	$⊢ f \in (S^{T}) \to S \in V$
17	16	adantl	$⊢ (J \in T \land f \in (S^{T})) \to S \in V$
18	7	simprd	$⊢ (J \in T \land f \in (S^{T})) \to T \in V$
19		difexg	$⊢ T \in V \to T ∖ \{J\} \in V$
20	18 19	syl	$⊢ (J \in T \land f \in (S^{T})) \to T ∖ \{J\} \in V$
21	17 20	elmapd	$⊢ (J \in T \land f \in (S^{T})) \to ({f ↾}_{(T ∖ \{J\})} \in (S^{(T ∖ \{J\})}) \leftrightarrow ({f ↾}_{(T ∖ \{J\})}) : T ∖ \{J\} ⟶ S)$
22	15 21	mpbird	$⊢ (J \in T \land f \in (S^{T})) \to {f ↾}_{(T ∖ \{J\})} \in (S^{(T ∖ \{J\})})$
23	10	ffnd	$⊢ (J \in T \land f \in (S^{T})) \to f Fn T$
24		fnsnsplit	$⊢ (f Fn T \land J \in T) \to f = ({f ↾}_{(T ∖ \{J\})}) \cup \{⟨J, f (J)⟩\}$
25	23 11 24	syl2anc	$⊢ (J \in T \land f \in (S^{T})) \to f = ({f ↾}_{(T ∖ \{J\})}) \cup \{⟨J, f (J)⟩\}$
26		opeq2	$⊢ y = f (J) \to ⟨J, y⟩ = ⟨J, f (J)⟩$
27	26	sneqd	$⊢ y = f (J) \to \{⟨J, y⟩\} = \{⟨J, f (J)⟩\}$
28	27	uneq2d	$⊢ y = f (J) \to g \cup \{⟨J, y⟩\} = g \cup \{⟨J, f (J)⟩\}$
29	28	eqeq2d	$⊢ y = f (J) \to (f = g \cup \{⟨J, y⟩\} \leftrightarrow f = g \cup \{⟨J, f (J)⟩\})$
30		uneq1	$⊢ g = {f ↾}_{(T ∖ \{J\})} \to g \cup \{⟨J, f (J)⟩\} = ({f ↾}_{(T ∖ \{J\})}) \cup \{⟨J, f (J)⟩\}$
31	30	eqeq2d	$⊢ g = {f ↾}_{(T ∖ \{J\})} \to (f = g \cup \{⟨J, f (J)⟩\} \leftrightarrow f = ({f ↾}_{(T ∖ \{J\})}) \cup \{⟨J, f (J)⟩\})$
32	29 31	rspc2ev	$⊢ (f (J) \in S \land {f ↾}_{(T ∖ \{J\})} \in (S^{(T ∖ \{J\})}) \land f = ({f ↾}_{(T ∖ \{J\})}) \cup \{⟨J, f (J)⟩\}) \to \exists y \in S \exists g \in (S^{(T ∖ \{J\})}) f = g \cup \{⟨J, y⟩\}$
33	12 22 25 32	syl3anc	$⊢ (J \in T \land f \in (S^{T})) \to \exists y \in S \exists g \in (S^{(T ∖ \{J\})}) f = g \cup \{⟨J, y⟩\}$
34	33	ex	$⊢ J \in T \to (f \in (S^{T}) \to \exists y \in S \exists g \in (S^{(T ∖ \{J\})}) f = g \cup \{⟨J, y⟩\})$
35		elmapi	$⊢ g \in (S^{(T ∖ \{J\})}) \to g : T ∖ \{J\} ⟶ S$
36	35	ad2antll	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to g : T ∖ \{J\} ⟶ S$
37		f1osng	$⊢ (J \in T \land y \in V) \to \{⟨J, y⟩\} : \{J\} \underset{1-1 onto}{⟶} \{y\}$
38		f1of	$⊢ \{⟨J, y⟩\} : \{J\} \underset{1-1 onto}{⟶} \{y\} \to \{⟨J, y⟩\} : \{J\} ⟶ \{y\}$
39	37 38	syl	$⊢ (J \in T \land y \in V) \to \{⟨J, y⟩\} : \{J\} ⟶ \{y\}$
40	39	elvd	$⊢ J \in T \to \{⟨J, y⟩\} : \{J\} ⟶ \{y\}$
41	40	adantr	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to \{⟨J, y⟩\} : \{J\} ⟶ \{y\}$
42		incom	$⊢ (T ∖ \{J\}) \cap \{J\} = \{J\} \cap (T ∖ \{J\})$
43		disjdif	$⊢ \{J\} \cap (T ∖ \{J\}) = \emptyset$
44	42 43	eqtri	$⊢ (T ∖ \{J\}) \cap \{J\} = \emptyset$
45	44	a1i	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (T ∖ \{J\}) \cap \{J\} = \emptyset$
46		fun	$⊢ ((g : T ∖ \{J\} ⟶ S \land \{⟨J, y⟩\} : \{J\} ⟶ \{y\}) \land (T ∖ \{J\}) \cap \{J\} = \emptyset) \to (g \cup \{⟨J, y⟩\}) : (T ∖ \{J\}) \cup \{J\} ⟶ S \cup \{y\}$
47	36 41 45 46	syl21anc	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (g \cup \{⟨J, y⟩\}) : (T ∖ \{J\}) \cup \{J\} ⟶ S \cup \{y\}$
48		uncom	$⊢ (T ∖ \{J\}) \cup \{J\} = \{J\} \cup (T ∖ \{J\})$
49		simpl	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to J \in T$
50	49	snssd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to \{J\} \subseteq T$
51		undif	$⊢ \{J\} \subseteq T \leftrightarrow \{J\} \cup (T ∖ \{J\}) = T$
52	50 51	sylib	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to \{J\} \cup (T ∖ \{J\}) = T$
53	48 52	syl5eq	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (T ∖ \{J\}) \cup \{J\} = T$
54	53	feq2d	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to ((g \cup \{⟨J, y⟩\}) : (T ∖ \{J\}) \cup \{J\} ⟶ S \cup \{y\} \leftrightarrow (g \cup \{⟨J, y⟩\}) : T ⟶ S \cup \{y\})$
55	47 54	mpbid	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (g \cup \{⟨J, y⟩\}) : T ⟶ S \cup \{y\}$
56		ssidd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to S \subseteq S$
57		snssi	$⊢ y \in S \to \{y\} \subseteq S$
58	57	ad2antrl	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to \{y\} \subseteq S$
59	56 58	unssd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to S \cup \{y\} \subseteq S$
60	55 59	fssd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (g \cup \{⟨J, y⟩\}) : T ⟶ S$
61		elmapex	$⊢ g \in (S^{(T ∖ \{J\})}) \to (S \in V \land T ∖ \{J\} \in V)$
62	61	ad2antll	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (S \in V \land T ∖ \{J\} \in V)$
63	62	simpld	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to S \in V$
64		ssun1	$⊢ T \subseteq T \cup \{J\}$
65		undif1	$⊢ (T ∖ \{J\}) \cup \{J\} = T \cup \{J\}$
66	62	simprd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to T ∖ \{J\} \in V$
67		snex	$⊢ \{J\} \in V$
68		unexg	$⊢ (T ∖ \{J\} \in V \land \{J\} \in V) \to (T ∖ \{J\}) \cup \{J\} \in V$
69	66 67 68	sylancl	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (T ∖ \{J\}) \cup \{J\} \in V$
70	65 69	eqeltrrid	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to T \cup \{J\} \in V$
71		ssexg	$⊢ (T \subseteq T \cup \{J\} \land T \cup \{J\} \in V) \to T \in V$
72	64 70 71	sylancr	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to T \in V$
73	63 72	elmapd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (g \cup \{⟨J, y⟩\} \in (S^{T}) \leftrightarrow (g \cup \{⟨J, y⟩\}) : T ⟶ S)$
74	60 73	mpbird	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to g \cup \{⟨J, y⟩\} \in (S^{T})$
75		eleq1	$⊢ f = g \cup \{⟨J, y⟩\} \to (f \in (S^{T}) \leftrightarrow g \cup \{⟨J, y⟩\} \in (S^{T}))$
76	74 75	syl5ibrcom	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (f = g \cup \{⟨J, y⟩\} \to f \in (S^{T}))$
77	76	rexlimdvva	$⊢ J \in T \to (\exists y \in S \exists g \in (S^{(T ∖ \{J\})}) f = g \cup \{⟨J, y⟩\} \to f \in (S^{T}))$
78	34 77	impbid	$⊢ J \in T \to (f \in (S^{T}) \leftrightarrow \exists y \in S \exists g \in (S^{(T ∖ \{J\})}) f = g \cup \{⟨J, y⟩\})$
79	1	adantl	$⊢ (J \in T \land f = g \cup \{⟨J, y⟩\}) \to (φ \leftrightarrow ψ)$
80	4 78 79	ralxpxfr2d	$⊢ J \in T \to (\forall f \in (S^{T}) φ \leftrightarrow \forall y \in S \forall g \in (S^{(T ∖ \{J\})}) ψ)$

Metamath Proof Explorer

Theorem ralxpmap

Proof