mclspps

Description: The closure is closed under application of provable pre-statements. (Compare mclsax .) This theorem is what justifies the treatment of theorems as "equivalent" to axioms once they have been proven: the composition of one theorem in the proof of another yields a theorem. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mclspps.d	$⊢ D = mDV (T)$
	mclspps.e	$⊢ E = mEx (T)$
	mclspps.c	$⊢ C = mCls (T)$
	mclspps.1	$⊢ φ \to T \in mFS$
	mclspps.2	$⊢ φ \to K \subseteq D$
	mclspps.3	$⊢ φ \to B \subseteq E$
	mclspps.j	$⊢ J = mPPSt (T)$
	mclspps.l	$⊢ L = mSubst (T)$
	mclspps.v	$⊢ V = mVR (T)$
	mclspps.h	$⊢ H = mVH (T)$
	mclspps.w	$⊢ W = mVars (T)$
	mclspps.4	$⊢ φ \to ⟨M, O, P⟩ \in J$
	mclspps.5	$⊢ φ \to S \in ran L$
	mclspps.6	$⊢ (φ \land x \in O) \to S (x) \in (K C B)$
	mclspps.7	$⊢ (φ \land v \in V) \to S (H (v)) \in (K C B)$
	mclspps.8	$⊢ (φ \land (x M y \land a \in W (S (H (x))) \land b \in W (S (H (y))))) \to a K b$
Assertion	mclspps	$⊢ φ \to S (P) \in (K C B)$

Proof

Step	Hyp	Ref	Expression
1		mclspps.d	$⊢ D = mDV (T)$
2		mclspps.e	$⊢ E = mEx (T)$
3		mclspps.c	$⊢ C = mCls (T)$
4		mclspps.1	$⊢ φ \to T \in mFS$
5		mclspps.2	$⊢ φ \to K \subseteq D$
6		mclspps.3	$⊢ φ \to B \subseteq E$
7		mclspps.j	$⊢ J = mPPSt (T)$
8		mclspps.l	$⊢ L = mSubst (T)$
9		mclspps.v	$⊢ V = mVR (T)$
10		mclspps.h	$⊢ H = mVH (T)$
11		mclspps.w	$⊢ W = mVars (T)$
12		mclspps.4	$⊢ φ \to ⟨M, O, P⟩ \in J$
13		mclspps.5	$⊢ φ \to S \in ran L$
14		mclspps.6	$⊢ (φ \land x \in O) \to S (x) \in (K C B)$
15		mclspps.7	$⊢ (φ \land v \in V) \to S (H (v)) \in (K C B)$
16		mclspps.8	$⊢ (φ \land (x M y \land a \in W (S (H (x))) \land b \in W (S (H (y))))) \to a K b$
17	8 2	msubf	$⊢ S \in ran L \to S : E ⟶ E$
18	13 17	syl	$⊢ φ \to S : E ⟶ E$
19	18	ffnd	$⊢ φ \to S Fn E$
20		eqid	$⊢ mPreSt (T) = mPreSt (T)$
21	20 7	mppspst	$⊢ J \subseteq mPreSt (T)$
22	21 12	sseldi	$⊢ φ \to ⟨M, O, P⟩ \in mPreSt (T)$
23	1 2 20	elmpst	$⊢ ⟨M, O, P⟩ \in mPreSt (T) \leftrightarrow ((M \subseteq D \land M^{-1} = M) \land (O \subseteq E \land O \in Fin) \land P \in E)$
24	22 23	sylib	$⊢ φ \to ((M \subseteq D \land M^{-1} = M) \land (O \subseteq E \land O \in Fin) \land P \in E)$
25	24	simp1d	$⊢ φ \to (M \subseteq D \land M^{-1} = M)$
26	25	simpld	$⊢ φ \to M \subseteq D$
27	24	simp2d	$⊢ φ \to (O \subseteq E \land O \in Fin)$
28	27	simpld	$⊢ φ \to O \subseteq E$
29		eqid	$⊢ mAx (T) = mAx (T)$
30	14	ralrimiva	$⊢ φ \to \forall x \in O S (x) \in (K C B)$
31	18	ffund	$⊢ φ \to Fun S$
32	18	fdmd	$⊢ φ \to dom S = E$
33	28 32	sseqtrrd	$⊢ φ \to O \subseteq dom S$
34		funimass5	$⊢ (Fun S \land O \subseteq dom S) \to (O \subseteq S^{-1} [K C B] \leftrightarrow \forall x \in O S (x) \in (K C B))$
35	31 33 34	syl2anc	$⊢ φ \to (O \subseteq S^{-1} [K C B] \leftrightarrow \forall x \in O S (x) \in (K C B))$
36	30 35	mpbird	$⊢ φ \to O \subseteq S^{-1} [K C B]$
37	9 2 10	mvhf	$⊢ T \in mFS \to H : V ⟶ E$
38	4 37	syl	$⊢ φ \to H : V ⟶ E$
39	38	ffvelrnda	$⊢ (φ \land v \in V) \to H (v) \in E$
40		elpreima	$⊢ S Fn E \to (H (v) \in S^{-1} [K C B] \leftrightarrow (H (v) \in E \land S (H (v)) \in (K C B)))$
41	19 40	syl	$⊢ φ \to (H (v) \in S^{-1} [K C B] \leftrightarrow (H (v) \in E \land S (H (v)) \in (K C B)))$
42	41	adantr	$⊢ (φ \land v \in V) \to (H (v) \in S^{-1} [K C B] \leftrightarrow (H (v) \in E \land S (H (v)) \in (K C B)))$
43	39 15 42	mpbir2and	$⊢ (φ \land v \in V) \to H (v) \in S^{-1} [K C B]$
44	4	3ad2ant1	$⊢ (φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \to T \in mFS$
45	5	3ad2ant1	$⊢ (φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \to K \subseteq D$
46	6	3ad2ant1	$⊢ (φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \to B \subseteq E$
47	12	3ad2ant1	$⊢ (φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \to ⟨M, O, P⟩ \in J$
48	13	3ad2ant1	$⊢ (φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \to S \in ran L$
49	14	3ad2antl1	$⊢ ((φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \land x \in O) \to S (x) \in (K C B)$
50	15	3ad2antl1	$⊢ ((φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \land v \in V) \to S (H (v)) \in (K C B)$
51	16	3ad2antl1	$⊢ ((φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \land (x M y \land a \in W (S (H (x))) \land b \in W (S (H (y))))) \to a K b$
52		simp21	$⊢ (φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \to ⟨m, o, p⟩ \in mAx (T)$
53		simp22	$⊢ (φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \to s \in ran L$
54		simp23	$⊢ (φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \to s [o \cup ran H] \subseteq S^{-1} [K C B]$
55		simp3	$⊢ (φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \to \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)$
56	1 2 3 44 45 46 7 8 9 10 11 47 48 49 50 51 52 53 54 55	mclsppslem	$⊢ (φ \land (⟨m, o, p⟩ \in mAx (T) \land s \in ran L \land s [o \cup ran H] \subseteq S^{-1} [K C B]) \land \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)) \to s (p) \in S^{-1} [K C B]$
57	1 2 3 4 26 28 29 8 9 10 11 36 43 56	mclsind	$⊢ φ \to M C O \subseteq S^{-1} [K C B]$
58	20 7 3	elmpps	$⊢ ⟨M, O, P⟩ \in J \leftrightarrow (⟨M, O, P⟩ \in mPreSt (T) \land P \in (M C O))$
59	58	simprbi	$⊢ ⟨M, O, P⟩ \in J \to P \in (M C O)$
60	12 59	syl	$⊢ φ \to P \in (M C O)$
61	57 60	sseldd	$⊢ φ \to P \in S^{-1} [K C B]$
62		elpreima	$⊢ S Fn E \to (P \in S^{-1} [K C B] \leftrightarrow (P \in E \land S (P) \in (K C B)))$
63	62	simplbda	$⊢ (S Fn E \land P \in S^{-1} [K C B]) \to S (P) \in (K C B)$
64	19 61 63	syl2anc	$⊢ φ \to S (P) \in (K C B)$

Metamath Proof Explorer

Theorem mclspps

Proof