mclsppslem

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$
	mclsppslem.9	$⊢ φ \to ⟨m, o, p⟩ \in mAx (T)$
	mclsppslem.10	$⊢ φ \to s \in ran L$
	mclsppslem.11	$⊢ φ \to s [o \cup ran H] \subseteq S^{-1} [K C B]$
	mclsppslem.12	$⊢ φ \to \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)$
Assertion	mclsppslem	$⊢ φ \to s (p) \in S^{-1} [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		mclsppslem.9	$⊢ φ \to ⟨m, o, p⟩ \in mAx (T)$
18		mclsppslem.10	$⊢ φ \to s \in ran L$
19		mclsppslem.11	$⊢ φ \to s [o \cup ran H] \subseteq S^{-1} [K C B]$
20		mclsppslem.12	$⊢ φ \to \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M)$
21	8 2	msubf	$⊢ s \in ran L \to s : E ⟶ E$
22	18 21	syl	$⊢ φ \to s : E ⟶ E$
23		eqid	$⊢ mAx (T) = mAx (T)$
24		eqid	$⊢ mStat (T) = mStat (T)$
25	23 24	maxsta	$⊢ T \in mFS \to mAx (T) \subseteq mStat (T)$
26	4 25	syl	$⊢ φ \to mAx (T) \subseteq mStat (T)$
27		eqid	$⊢ mPreSt (T) = mPreSt (T)$
28	27 24	mstapst	$⊢ mStat (T) \subseteq mPreSt (T)$
29	26 28	sstrdi	$⊢ φ \to mAx (T) \subseteq mPreSt (T)$
30	29 17	sseldd	$⊢ φ \to ⟨m, o, p⟩ \in mPreSt (T)$
31	1 2 27	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)$
32	30 31	sylib	$⊢ φ \to ((m \subseteq D \land m^{-1} = m) \land (o \subseteq E \land o \in Fin) \land p \in E)$
33	32	simp3d	$⊢ φ \to p \in E$
34	22 33	ffvelrnd	$⊢ φ \to s (p) \in E$
35		fvco3	$⊢ (s : E ⟶ E \land p \in E) \to (S \circ s) (p) = S (s (p))$
36	22 33 35	syl2anc	$⊢ φ \to (S \circ s) (p) = S (s (p))$
37	8	msubco	$⊢ (S \in ran L \land s \in ran L) \to S \circ s \in ran L$
38	13 18 37	syl2anc	$⊢ φ \to S \circ s \in ran L$
39	8 2	msubf	$⊢ S \in ran L \to S : E ⟶ E$
40	13 39	syl	$⊢ φ \to S : E ⟶ E$
41		fco	$⊢ (S : E ⟶ E \land s : E ⟶ E) \to (S \circ s) : E ⟶ E$
42	40 22 41	syl2anc	$⊢ φ \to (S \circ s) : E ⟶ E$
43	42	ffnd	$⊢ φ \to (S \circ s) Fn E$
44	43	adantr	$⊢ (φ \land c \in o) \to (S \circ s) Fn E$
45	22	ffund	$⊢ φ \to Fun s$
46	31	simp2bi	$⊢ ⟨m, o, p⟩ \in mPreSt (T) \to (o \subseteq E \land o \in Fin)$
47	30 46	syl	$⊢ φ \to (o \subseteq E \land o \in Fin)$
48	47	simpld	$⊢ φ \to o \subseteq E$
49	9 2 10	mvhf	$⊢ T \in mFS \to H : V ⟶ E$
50		frn	$⊢ H : V ⟶ E \to ran H \subseteq E$
51	4 49 50	3syl	$⊢ φ \to ran H \subseteq E$
52	48 51	unssd	$⊢ φ \to o \cup ran H \subseteq E$
53	22	fdmd	$⊢ φ \to dom s = E$
54	52 53	sseqtrrd	$⊢ φ \to o \cup ran H \subseteq dom s$
55		funimass3	$⊢ (Fun s \land o \cup ran H \subseteq dom s) \to (s [o \cup ran H] \subseteq S^{-1} [K C B] \leftrightarrow o \cup ran H \subseteq s^{-1} [S^{-1} [K C B]])$
56	45 54 55	syl2anc	$⊢ φ \to (s [o \cup ran H] \subseteq S^{-1} [K C B] \leftrightarrow o \cup ran H \subseteq s^{-1} [S^{-1} [K C B]])$
57	19 56	mpbid	$⊢ φ \to o \cup ran H \subseteq s^{-1} [S^{-1} [K C B]]$
58		cnvco	$⊢ {(S \circ s)}^{-1} = s^{-1} \circ S^{-1}$
59	58	imaeq1i	$⊢ {(S \circ s)}^{-1} [K C B] = (s^{-1} \circ S^{-1}) [K C B]$
60		imaco	$⊢ (s^{-1} \circ S^{-1}) [K C B] = s^{-1} [S^{-1} [K C B]]$
61	59 60	eqtri	$⊢ {(S \circ s)}^{-1} [K C B] = s^{-1} [S^{-1} [K C B]]$
62	57 61	sseqtrrdi	$⊢ φ \to o \cup ran H \subseteq {(S \circ s)}^{-1} [K C B]$
63	62	unssad	$⊢ φ \to o \subseteq {(S \circ s)}^{-1} [K C B]$
64	63	sselda	$⊢ (φ \land c \in o) \to c \in {(S \circ s)}^{-1} [K C B]$
65		elpreima	$⊢ (S \circ s) Fn E \to (c \in {(S \circ s)}^{-1} [K C B] \leftrightarrow (c \in E \land (S \circ s) (c) \in (K C B)))$
66	65	simplbda	$⊢ ((S \circ s) Fn E \land c \in {(S \circ s)}^{-1} [K C B]) \to (S \circ s) (c) \in (K C B)$
67	44 64 66	syl2anc	$⊢ (φ \land c \in o) \to (S \circ s) (c) \in (K C B)$
68	43	adantr	$⊢ (φ \land t \in V) \to (S \circ s) Fn E$
69	62	unssbd	$⊢ φ \to ran H \subseteq {(S \circ s)}^{-1} [K C B]$
70	69	adantr	$⊢ (φ \land t \in V) \to ran H \subseteq {(S \circ s)}^{-1} [K C B]$
71		ffn	$⊢ H : V ⟶ E \to H Fn V$
72	4 49 71	3syl	$⊢ φ \to H Fn V$
73		fnfvelrn	$⊢ (H Fn V \land t \in V) \to H (t) \in ran H$
74	72 73	sylan	$⊢ (φ \land t \in V) \to H (t) \in ran H$
75	70 74	sseldd	$⊢ (φ \land t \in V) \to H (t) \in {(S \circ s)}^{-1} [K C B]$
76		elpreima	$⊢ (S \circ s) Fn E \to (H (t) \in {(S \circ s)}^{-1} [K C B] \leftrightarrow (H (t) \in E \land (S \circ s) (H (t)) \in (K C B)))$
77	76	simplbda	$⊢ ((S \circ s) Fn E \land H (t) \in {(S \circ s)}^{-1} [K C B]) \to (S \circ s) (H (t)) \in (K C B)$
78	68 75 77	syl2anc	$⊢ (φ \land t \in V) \to (S \circ s) (H (t)) \in (K C B)$
79	22	adantr	$⊢ (φ \land c m d) \to s : E ⟶ E$
80	4 49	syl	$⊢ φ \to H : V ⟶ E$
81	80	adantr	$⊢ (φ \land c m d) \to H : V ⟶ E$
82	32	simp1d	$⊢ φ \to (m \subseteq D \land m^{-1} = m)$
83	82	simpld	$⊢ φ \to m \subseteq D$
84	9 1	mdvval	$⊢ D = (V \times V) ∖ I$
85		difss	$⊢ (V \times V) ∖ I \subseteq V \times V$
86	84 85	eqsstri	$⊢ D \subseteq V \times V$
87	83 86	sstrdi	$⊢ φ \to m \subseteq V \times V$
88	87	ssbrd	$⊢ φ \to (c m d \to c (V \times V) d)$
89	88	imp	$⊢ (φ \land c m d) \to c (V \times V) d$
90		brxp	$⊢ c (V \times V) d \leftrightarrow (c \in V \land d \in V)$
91	89 90	sylib	$⊢ (φ \land c m d) \to (c \in V \land d \in V)$
92	91	simpld	$⊢ (φ \land c m d) \to c \in V$
93	81 92	ffvelrnd	$⊢ (φ \land c m d) \to H (c) \in E$
94		fvco3	$⊢ (s : E ⟶ E \land H (c) \in E) \to (S \circ s) (H (c)) = S (s (H (c)))$
95	79 93 94	syl2anc	$⊢ (φ \land c m d) \to (S \circ s) (H (c)) = S (s (H (c)))$
96	95	fveq2d	$⊢ (φ \land c m d) \to W ((S \circ s) (H (c))) = W (S (s (H (c))))$
97	4	adantr	$⊢ (φ \land c m d) \to T \in mFS$
98	13	adantr	$⊢ (φ \land c m d) \to S \in ran L$
99	79 93	ffvelrnd	$⊢ (φ \land c m d) \to s (H (c)) \in E$
100	8 2 11 10	msubvrs	$⊢ (T \in mFS \land S \in ran L \land s (H (c)) \in E) \to W (S (s (H (c)))) = ⋃_{u \in W (s (H (c)))} W (S (H (u)))$
101	97 98 99 100	syl3anc	$⊢ (φ \land c m d) \to W (S (s (H (c)))) = ⋃_{u \in W (s (H (c)))} W (S (H (u)))$
102	96 101	eqtrd	$⊢ (φ \land c m d) \to W ((S \circ s) (H (c))) = ⋃_{u \in W (s (H (c)))} W (S (H (u)))$
103	102	eleq2d	$⊢ (φ \land c m d) \to (a \in W ((S \circ s) (H (c))) \leftrightarrow a \in ⋃_{u \in W (s (H (c)))} W (S (H (u))))$
104		eliun	$⊢ a \in ⋃_{u \in W (s (H (c)))} W (S (H (u))) \leftrightarrow \exists u \in W (s (H (c))) a \in W (S (H (u)))$
105	103 104	bitrdi	$⊢ (φ \land c m d) \to (a \in W ((S \circ s) (H (c))) \leftrightarrow \exists u \in W (s (H (c))) a \in W (S (H (u))))$
106	91	simprd	$⊢ (φ \land c m d) \to d \in V$
107	81 106	ffvelrnd	$⊢ (φ \land c m d) \to H (d) \in E$
108		fvco3	$⊢ (s : E ⟶ E \land H (d) \in E) \to (S \circ s) (H (d)) = S (s (H (d)))$
109	79 107 108	syl2anc	$⊢ (φ \land c m d) \to (S \circ s) (H (d)) = S (s (H (d)))$
110	109	fveq2d	$⊢ (φ \land c m d) \to W ((S \circ s) (H (d))) = W (S (s (H (d))))$
111	79 107	ffvelrnd	$⊢ (φ \land c m d) \to s (H (d)) \in E$
112	8 2 11 10	msubvrs	$⊢ (T \in mFS \land S \in ran L \land s (H (d)) \in E) \to W (S (s (H (d)))) = ⋃_{v \in W (s (H (d)))} W (S (H (v)))$
113	97 98 111 112	syl3anc	$⊢ (φ \land c m d) \to W (S (s (H (d)))) = ⋃_{v \in W (s (H (d)))} W (S (H (v)))$
114	110 113	eqtrd	$⊢ (φ \land c m d) \to W ((S \circ s) (H (d))) = ⋃_{v \in W (s (H (d)))} W (S (H (v)))$
115	114	eleq2d	$⊢ (φ \land c m d) \to (b \in W ((S \circ s) (H (d))) \leftrightarrow b \in ⋃_{v \in W (s (H (d)))} W (S (H (v))))$
116		eliun	$⊢ b \in ⋃_{v \in W (s (H (d)))} W (S (H (v))) \leftrightarrow \exists v \in W (s (H (d))) b \in W (S (H (v)))$
117	115 116	bitrdi	$⊢ (φ \land c m d) \to (b \in W ((S \circ s) (H (d))) \leftrightarrow \exists v \in W (s (H (d))) b \in W (S (H (v))))$
118	105 117	anbi12d	$⊢ (φ \land c m d) \to ((a \in W ((S \circ s) (H (c))) \land b \in W ((S \circ s) (H (d)))) \leftrightarrow (\exists u \in W (s (H (c))) a \in W (S (H (u))) \land \exists v \in W (s (H (d))) b \in W (S (H (v)))))$
119		reeanv	$⊢ \exists u \in W (s (H (c))) \exists v \in W (s (H (d))) (a \in W (S (H (u))) \land b \in W (S (H (v)))) \leftrightarrow (\exists u \in W (s (H (c))) a \in W (S (H (u))) \land \exists v \in W (s (H (d))) b \in W (S (H (v))))$
120		simpll	$⊢ ((φ \land c m d) \land (u \in W (s (H (c))) \land v \in W (s (H (d))))) \to φ$
121		brxp	$⊢ u (W (s (H (c))) \times W (s (H (d)))) v \leftrightarrow (u \in W (s (H (c))) \land v \in W (s (H (d))))$
122		breq12	$⊢ (z = c \land w = d) \to (z m w \leftrightarrow c m d)$
123		simpl	$⊢ (z = c \land w = d) \to z = c$
124	123	fveq2d	$⊢ (z = c \land w = d) \to H (z) = H (c)$
125	124	fveq2d	$⊢ (z = c \land w = d) \to s (H (z)) = s (H (c))$
126	125	fveq2d	$⊢ (z = c \land w = d) \to W (s (H (z))) = W (s (H (c)))$
127		simpr	$⊢ (z = c \land w = d) \to w = d$
128	127	fveq2d	$⊢ (z = c \land w = d) \to H (w) = H (d)$
129	128	fveq2d	$⊢ (z = c \land w = d) \to s (H (w)) = s (H (d))$
130	129	fveq2d	$⊢ (z = c \land w = d) \to W (s (H (w))) = W (s (H (d)))$
131	126 130	xpeq12d	$⊢ (z = c \land w = d) \to W (s (H (z))) \times W (s (H (w))) = W (s (H (c))) \times W (s (H (d)))$
132	131	sseq1d	$⊢ (z = c \land w = d) \to (W (s (H (z))) \times W (s (H (w))) \subseteq M \leftrightarrow W (s (H (c))) \times W (s (H (d))) \subseteq M)$
133	122 132	imbi12d	$⊢ (z = c \land w = d) \to ((z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M) \leftrightarrow (c m d \to W (s (H (c))) \times W (s (H (d))) \subseteq M))$
134	133	spc2gv	$⊢ (c \in V \land d \in V) \to (\forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M) \to (c m d \to W (s (H (c))) \times W (s (H (d))) \subseteq M))$
135	134	el2v	$⊢ \forall z \forall w (z m w \to W (s (H (z))) \times W (s (H (w))) \subseteq M) \to (c m d \to W (s (H (c))) \times W (s (H (d))) \subseteq M)$
136	20 135	syl	$⊢ φ \to (c m d \to W (s (H (c))) \times W (s (H (d))) \subseteq M)$
137	136	imp	$⊢ (φ \land c m d) \to W (s (H (c))) \times W (s (H (d))) \subseteq M$
138	137	ssbrd	$⊢ (φ \land c m d) \to (u (W (s (H (c))) \times W (s (H (d)))) v \to u M v)$
139	121 138	syl5bir	$⊢ (φ \land c m d) \to ((u \in W (s (H (c))) \land v \in W (s (H (d)))) \to u M v)$
140	139	imp	$⊢ ((φ \land c m d) \land (u \in W (s (H (c))) \land v \in W (s (H (d))))) \to u M v$
141		vex	$⊢ u \in V$
142		vex	$⊢ v \in V$
143		breq12	$⊢ (x = u \land y = v) \to (x M y \leftrightarrow u M v)$
144		simpl	$⊢ (x = u \land y = v) \to x = u$
145	144	fveq2d	$⊢ (x = u \land y = v) \to H (x) = H (u)$
146	145	fveq2d	$⊢ (x = u \land y = v) \to S (H (x)) = S (H (u))$
147	146	fveq2d	$⊢ (x = u \land y = v) \to W (S (H (x))) = W (S (H (u)))$
148	147	eleq2d	$⊢ (x = u \land y = v) \to (a \in W (S (H (x))) \leftrightarrow a \in W (S (H (u))))$
149		simpr	$⊢ (x = u \land y = v) \to y = v$
150	149	fveq2d	$⊢ (x = u \land y = v) \to H (y) = H (v)$
151	150	fveq2d	$⊢ (x = u \land y = v) \to S (H (y)) = S (H (v))$
152	151	fveq2d	$⊢ (x = u \land y = v) \to W (S (H (y))) = W (S (H (v)))$
153	152	eleq2d	$⊢ (x = u \land y = v) \to (b \in W (S (H (y))) \leftrightarrow b \in W (S (H (v))))$
154	143 148 153	3anbi123d	$⊢ (x = u \land y = v) \to ((x M y \land a \in W (S (H (x))) \land b \in W (S (H (y)))) \leftrightarrow (u M v \land a \in W (S (H (u))) \land b \in W (S (H (v)))))$
155	154	anbi2d	$⊢ (x = u \land y = v) \to ((φ \land (x M y \land a \in W (S (H (x))) \land b \in W (S (H (y))))) \leftrightarrow (φ \land (u M v \land a \in W (S (H (u))) \land b \in W (S (H (v))))))$
156	155	imbi1d	$⊢ (x = u \land y = v) \to (((φ \land (x M y \land a \in W (S (H (x))) \land b \in W (S (H (y))))) \to a K b) \leftrightarrow ((φ \land (u M v \land a \in W (S (H (u))) \land b \in W (S (H (v))))) \to a K b))$
157	141 142 156 16	vtocl2	$⊢ (φ \land (u M v \land a \in W (S (H (u))) \land b \in W (S (H (v))))) \to a K b$
158	157	3exp2	$⊢ φ \to (u M v \to (a \in W (S (H (u))) \to (b \in W (S (H (v))) \to a K b)))$
159	158	imp4b	$⊢ (φ \land u M v) \to ((a \in W (S (H (u))) \land b \in W (S (H (v)))) \to a K b)$
160	120 140 159	syl2anc	$⊢ ((φ \land c m d) \land (u \in W (s (H (c))) \land v \in W (s (H (d))))) \to ((a \in W (S (H (u))) \land b \in W (S (H (v)))) \to a K b)$
161	160	rexlimdvva	$⊢ (φ \land c m d) \to (\exists u \in W (s (H (c))) \exists v \in W (s (H (d))) (a \in W (S (H (u))) \land b \in W (S (H (v)))) \to a K b)$
162	119 161	syl5bir	$⊢ (φ \land c m d) \to ((\exists u \in W (s (H (c))) a \in W (S (H (u))) \land \exists v \in W (s (H (d))) b \in W (S (H (v)))) \to a K b)$
163	118 162	sylbid	$⊢ (φ \land c m d) \to ((a \in W ((S \circ s) (H (c))) \land b \in W ((S \circ s) (H (d)))) \to a K b)$
164	163	exp4b	$⊢ φ \to (c m d \to (a \in W ((S \circ s) (H (c))) \to (b \in W ((S \circ s) (H (d))) \to a K b)))$
165	164	3imp2	$⊢ (φ \land (c m d \land a \in W ((S \circ s) (H (c))) \land b \in W ((S \circ s) (H (d))))) \to a K b$
166	1 2 3 4 5 6 23 8 9 10 11 17 38 67 78 165	mclsax	$⊢ φ \to (S \circ s) (p) \in (K C B)$
167	36 166	eqeltrrd	$⊢ φ \to S (s (p)) \in (K C B)$
168	40	ffnd	$⊢ φ \to S Fn E$
169		elpreima	$⊢ S Fn E \to (s (p) \in S^{-1} [K C B] \leftrightarrow (s (p) \in E \land S (s (p)) \in (K C B)))$
170	168 169	syl	$⊢ φ \to (s (p) \in S^{-1} [K C B] \leftrightarrow (s (p) \in E \land S (s (p)) \in (K C B)))$
171	34 167 170	mpbir2and	$⊢ φ \to s (p) \in S^{-1} [K C B]$

Metamath Proof Explorer

Theorem mclsppslem

Proof