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	ffvelcdmd	$⊢ (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		simpl	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to J \in T$
46	45	snssd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to \{J\} \subseteq T$
47		undifr	$⊢ \{J\} \subseteq T \leftrightarrow (T ∖ \{J\}) \cup \{J\} = T$
48	46 47	sylib	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (T ∖ \{J\}) \cup \{J\} = T$
49	48	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\})$
50	44 49	mpbid	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (g \cup \{⟨J, y⟩\}) : T ⟶ S \cup \{y\}$
51		ssidd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to S \subseteq S$
52		snssi	$⊢ y \in S \to \{y\} \subseteq S$
53	52	ad2antrl	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to \{y\} \subseteq S$
54	51 53	unssd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to S \cup \{y\} \subseteq S$
55	50 54	fssd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (g \cup \{⟨J, y⟩\}) : T ⟶ S$
56		elmapex	$⊢ g \in (S^{(T ∖ \{J\})}) \to (S \in V \land T ∖ \{J\} \in V)$
57	56	ad2antll	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (S \in V \land T ∖ \{J\} \in V)$
58	57	simpld	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to S \in V$
59		ssun1	$⊢ T \subseteq T \cup \{J\}$
60		undif1	$⊢ (T ∖ \{J\}) \cup \{J\} = T \cup \{J\}$
61	57	simprd	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to T ∖ \{J\} \in V$
62		snex	$⊢ \{J\} \in V$
63		unexg	$⊢ (T ∖ \{J\} \in V \land \{J\} \in V) \to (T ∖ \{J\}) \cup \{J\} \in V$
64	61 62 63	sylancl	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to (T ∖ \{J\}) \cup \{J\} \in V$
65	60 64	eqeltrrid	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to T \cup \{J\} \in V$
66		ssexg	$⊢ (T \subseteq T \cup \{J\} \land T \cup \{J\} \in V) \to T \in V$
67	59 65 66	sylancr	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to T \in V$
68	58 67	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)$
69	55 68	mpbird	$⊢ (J \in T \land (y \in S \land g \in (S^{(T ∖ \{J\})}))) \to g \cup \{⟨J, y⟩\} \in (S^{T})$
70		eleq1	$⊢ f = g \cup \{⟨J, y⟩\} \to (f \in (S^{T}) \leftrightarrow g \cup \{⟨J, y⟩\} \in (S^{T}))$
71	69 70	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}))$
72	71	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}))$
73	33 72	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⟩\})$
74	1	adantl	$⊢ (J \in T \land f = g \cup \{⟨J, y⟩\}) \to (φ \leftrightarrow ψ)$
75	4 73 74	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