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	18	difexd	$⊢ (J \in T \land f \in (S^{T})) \to T ∖ \{J\} \in V$
20	17 19	elmapd	$⊢ (J \in T \land f \in (S^{T})) \to ({f ↾}_{(T ∖ \{J\})} \in (S^{(T ∖ \{J\})}) \leftrightarrow ({f ↾}_{(T ∖ \{J\})}) : T ∖ \{J\} ⟶ S)$
21	15 20	mpbird	$⊢ (J \in T \land f \in (S^{T})) \to {f ↾}_{(T ∖ \{J\})} \in (S^{(T ∖ \{J\})})$
22	10	ffnd	$⊢ (J \in T \land f \in (S^{T})) \to f Fn T$
23		fnsnsplit	$⊢ (f Fn T \land J \in T) \to f = ({f ↾}_{(T ∖ \{J\})}) \cup \{⟨J, f (J)⟩\}$
24	22 11 23	syl2anc	$⊢ (J \in T \land f \in (S^{T})) \to f = ({f ↾}_{(T ∖ \{J\})}) \cup \{⟨J, f (J)⟩\}$
25		opeq2	$⊢ y = f (J) \to ⟨J, y⟩ = ⟨J, f (J)⟩$
26	25	sneqd	$⊢ y = f (J) \to \{⟨J, y⟩\} = \{⟨J, f (J)⟩\}$
27	26	uneq2d	$⊢ y = f (J) \to g \cup \{⟨J, y⟩\} = g \cup \{⟨J, f (J)⟩\}$
28	27	eqeq2d	$⊢ y = f (J) \to (f = g \cup \{⟨J, y⟩\} \leftrightarrow f = g \cup \{⟨J, f (J)⟩\})$
29		uneq1	$⊢ g = {f ↾}_{(T ∖ \{J\})} \to g \cup \{⟨J, f (J)⟩\} = ({f ↾}_{(T ∖ \{J\})}) \cup \{⟨J, f (J)⟩\}$
30	29	eqeq2d	$⊢ g = {f ↾}_{(T ∖ \{J\})} \to (f = g \cup \{⟨J, f (J)⟩\} \leftrightarrow f = ({f ↾}_{(T ∖ \{J\})}) \cup \{⟨J, f (J)⟩\})$
31	28 30	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⟩\}$
32	12 21 24 31	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⟩\}$
33	32	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⟩\})$
34		elmapi	$⊢ g \in (S^{(T ∖ \{J\})}) \to g : T ∖ \{J\} ⟶ S$
35	34	ad2antll	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to g : T ∖ \{J\} ⟶ S$
36		f1osng	$⊢ (J \in T \land y \in V) \to \{⟨J, y⟩\} : \{J\} \underset{1-1 onto}{⟶} \{y\}$
37		f1of	$⊢ \{⟨J, y⟩\} : \{J\} \underset{1-1 onto}{⟶} \{y\} \to \{⟨J, y⟩\} : \{J\} ⟶ \{y\}$
38	36 37	syl	$⊢ (J \in T \land y \in V) \to \{⟨J, y⟩\} : \{J\} ⟶ \{y\}$
39	38	elvd	$⊢ J \in T \to \{⟨J, y⟩\} : \{J\} ⟶ \{y\}$
40	39	adantr	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to \{⟨J, y⟩\} : \{J\} ⟶ \{y\}$
41		disjdifr	$⊢ (T ∖ \{J\}) \cap \{J\} = \emptyset$
42	41	a1i	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (T ∖ \{J\}) \cap \{J\} = \emptyset$
43		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\}$
44	35 40 42 43	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\}$
45		uncom	$⊢ (T ∖ \{J\}) \cup \{J\} = \{J\} \cup (T ∖ \{J\})$
46		simpl	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to J \in T$
47	46	snssd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to \{J\} \subseteq T$
48		undif	$⊢ \{J\} \subseteq T \leftrightarrow \{J\} \cup (T ∖ \{J\}) = T$
49	47 48	sylib	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to \{J\} \cup (T ∖ \{J\}) = T$
50	45 49	eqtrid	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (T ∖ \{J\}) \cup \{J\} = T$
51	50	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\})$
52	44 51	mpbid	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (g \cup \{⟨J, y⟩\}) : T ⟶ S \cup \{y\}$
53		ssidd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to S \subseteq S$
54		snssi	$⊢ y \in S \to \{y\} \subseteq S$
55	54	ad2antrl	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to \{y\} \subseteq S$
56	53 55	unssd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to S \cup \{y\} \subseteq S$
57	52 56	fssd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (g \cup \{⟨J, y⟩\}) : T ⟶ S$
58		elmapex	$⊢ g \in (S^{(T ∖ \{J\})}) \to (S \in V \land T ∖ \{J\} \in V)$
59	58	ad2antll	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (S \in V \land T ∖ \{J\} \in V)$
60	59	simpld	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to S \in V$
61		ssun1	$⊢ T \subseteq T \cup \{J\}$
62		undif1	$⊢ (T ∖ \{J\}) \cup \{J\} = T \cup \{J\}$
63	59	simprd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to T ∖ \{J\} \in V$
64		snex	$⊢ \{J\} \in V$
65		unexg	$⊢ (T ∖ \{J\} \in V \land \{J\} \in V) \to (T ∖ \{J\}) \cup \{J\} \in V$
66	63 64 65	sylancl	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (T ∖ \{J\}) \cup \{J\} \in V$
67	62 66	eqeltrrid	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to T \cup \{J\} \in V$
68		ssexg	$⊢ (T \subseteq T \cup \{J\} \land T \cup \{J\} \in V) \to T \in V$
69	61 67 68	sylancr	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to T \in V$
70	60 69	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)$
71	57 70	mpbird	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to g \cup \{⟨J, y⟩\} \in (S^{T})$
72		eleq1	$⊢ f = g \cup \{⟨J, y⟩\} \to (f \in (S^{T}) \leftrightarrow g \cup \{⟨J, y⟩\} \in (S^{T}))$
73	71 72	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}))$
74	73	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}))$
75	33 74	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⟩\})$
76	1	adantl	$⊢ (J \in T \land f = g \cup \{⟨J, y⟩\}) \to (φ \leftrightarrow ψ)$
77	4 75 76	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