mclsind

Description: Induction theorem for closure: any other set Q closed under the axioms and the hypotheses contains all the elements of the closure. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mclsval.d	$⊢ D = mDV (T)$
	mclsval.e	$⊢ E = mEx (T)$
	mclsval.c	$⊢ C = mCls (T)$
	mclsval.1	$⊢ φ \to T \in mFS$
	mclsval.2	$⊢ φ \to K \subseteq D$
	mclsval.3	$⊢ φ \to B \subseteq E$
	mclsax.a	$⊢ A = mAx (T)$
	mclsax.l	$⊢ L = mSubst (T)$
	mclsax.v	$⊢ V = mVR (T)$
	mclsax.h	$⊢ H = mVH (T)$
	mclsax.w	$⊢ W = mVars (T)$
	mclsind.4	$⊢ φ \to B \subseteq Q$
	mclsind.5	$⊢ (φ \land v \in V) \to H (v) \in Q$
	mclsind.6	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q) \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in Q$
Assertion	mclsind	$⊢ φ \to K C B \subseteq Q$

Proof

Step	Hyp	Ref	Expression
1		mclsval.d	$⊢ D = mDV (T)$
2		mclsval.e	$⊢ E = mEx (T)$
3		mclsval.c	$⊢ C = mCls (T)$
4		mclsval.1	$⊢ φ \to T \in mFS$
5		mclsval.2	$⊢ φ \to K \subseteq D$
6		mclsval.3	$⊢ φ \to B \subseteq E$
7		mclsax.a	$⊢ A = mAx (T)$
8		mclsax.l	$⊢ L = mSubst (T)$
9		mclsax.v	$⊢ V = mVR (T)$
10		mclsax.h	$⊢ H = mVH (T)$
11		mclsax.w	$⊢ W = mVars (T)$
12		mclsind.4	$⊢ φ \to B \subseteq Q$
13		mclsind.5	$⊢ (φ \land v \in V) \to H (v) \in Q$
14		mclsind.6	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q) \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in Q$
15	1 2 3 4 5 6 10 7 8 11	mclsval	$⊢ φ \to K C B = ⋂ \{c \| (B \cup ran H \subseteq c \land \forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c)))\}$
16	6 12	ssind	$⊢ φ \to B \subseteq E \cap Q$
17	9 2 10	mvhf	$⊢ T \in mFS \to H : V ⟶ E$
18	4 17	syl	$⊢ φ \to H : V ⟶ E$
19	18	ffnd	$⊢ φ \to H Fn V$
20	18	ffvelcdmda	$⊢ (φ \land v \in V) \to H (v) \in E$
21	20 13	elind	$⊢ (φ \land v \in V) \to H (v) \in (E \cap Q)$
22	21	ralrimiva	$⊢ φ \to \forall v \in V H (v) \in (E \cap Q)$
23		ffnfv	$⊢ H : V ⟶ E \cap Q \leftrightarrow (H Fn V \land \forall v \in V H (v) \in (E \cap Q))$
24	19 22 23	sylanbrc	$⊢ φ \to H : V ⟶ E \cap Q$
25	24	frnd	$⊢ φ \to ran H \subseteq E \cap Q$
26	16 25	unssd	$⊢ φ \to B \cup ran H \subseteq E \cap Q$
27		id	$⊢ s [o \cup ran H] \subseteq E \cap Q \to s [o \cup ran H] \subseteq E \cap Q$
28		inss2	$⊢ E \cap Q \subseteq Q$
29	27 28	sstrdi	$⊢ s [o \cup ran H] \subseteq E \cap Q \to s [o \cup ran H] \subseteq Q$
30	4	adantr	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q)) \to T \in mFS$
31		eqid	$⊢ mREx (T) = mREx (T)$
32	9 31 8 2	msubff	$⊢ T \in mFS \to L : mREx (T) ↑_{𝑝𝑚} V ⟶ E^{E}$
33		frn	$⊢ L : mREx (T) ↑_{𝑝𝑚} V ⟶ E^{E} \to ran L \subseteq E^{E}$
34	30 32 33	3syl	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q)) \to ran L \subseteq E^{E}$
35		simpr2	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q)) \to s \in ran L$
36	34 35	sseldd	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q)) \to s \in (E^{E})$
37		elmapi	$⊢ s \in (E^{E}) \to s : E ⟶ E$
38	36 37	syl	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q)) \to s : E ⟶ E$
39		eqid	$⊢ mStat (T) = mStat (T)$
40	7 39	maxsta	$⊢ T \in mFS \to A \subseteq mStat (T)$
41	30 40	syl	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q)) \to A \subseteq mStat (T)$
42		eqid	$⊢ mPreSt (T) = mPreSt (T)$
43	42 39	mstapst	$⊢ mStat (T) \subseteq mPreSt (T)$
44	41 43	sstrdi	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q)) \to A \subseteq mPreSt (T)$
45		simpr1	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q)) \to ⟨m, o, p⟩ \in A$
46	44 45	sseldd	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q)) \to ⟨m, o, p⟩ \in mPreSt (T)$
47	1 2 42	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)$
48	47	simp3bi	$⊢ ⟨m, o, p⟩ \in mPreSt (T) \to p \in E$
49	46 48	syl	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q)) \to p \in E$
50	38 49	ffvelcdmd	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q)) \to s (p) \in E$
51	50	3adant3	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q) \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in E$
52	51 14	elind	$⊢ (φ \land (⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q) \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q)$
53	52	3exp	$⊢ φ \to ((⟨m, o, p⟩ \in A \land s \in ran L \land s [o \cup ran H] \subseteq Q) \to (\forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K) \to s (p) \in (E \cap Q)))$
54	53	3expd	$⊢ φ \to (⟨m, o, p⟩ \in A \to (s \in ran L \to (s [o \cup ran H] \subseteq Q \to (\forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K) \to s (p) \in (E \cap Q)))))$
55	54	imp31	$⊢ ((φ \land ⟨m, o, p⟩ \in A) \land s \in ran L) \to (s [o \cup ran H] \subseteq Q \to (\forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K) \to s (p) \in (E \cap Q)))$
56	29 55	syl5	$⊢ ((φ \land ⟨m, o, p⟩ \in A) \land s \in ran L) \to (s [o \cup ran H] \subseteq E \cap Q \to (\forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K) \to s (p) \in (E \cap Q)))$
57	56	impd	$⊢ ((φ \land ⟨m, o, p⟩ \in A) \land s \in ran L) \to ((s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q))$
58	57	ralrimiva	$⊢ (φ \land ⟨m, o, p⟩ \in A) \to \forall s \in ran L ((s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q))$
59	58	ex	$⊢ φ \to (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q)))$
60	59	alrimiv	$⊢ φ \to \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q)))$
61	60	alrimivv	$⊢ φ \to \forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q)))$
62	2	fvexi	$⊢ E \in V$
63	62	inex1	$⊢ E \cap Q \in V$
64		sseq2	$⊢ c = E \cap Q \to (B \cup ran H \subseteq c \leftrightarrow B \cup ran H \subseteq E \cap Q)$
65		sseq2	$⊢ c = E \cap Q \to (s [o \cup ran H] \subseteq c \leftrightarrow s [o \cup ran H] \subseteq E \cap Q)$
66	65	anbi1d	$⊢ c = E \cap Q \to ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \leftrightarrow (s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)))$
67		eleq2	$⊢ c = E \cap Q \to (s (p) \in c \leftrightarrow s (p) \in (E \cap Q))$
68	66 67	imbi12d	$⊢ c = E \cap Q \to (((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c) \leftrightarrow ((s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q)))$
69	68	ralbidv	$⊢ c = E \cap Q \to (\forall s \in ran L ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c) \leftrightarrow \forall s \in ran L ((s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q)))$
70	69	imbi2d	$⊢ c = E \cap Q \to ((⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c)) \leftrightarrow (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q))))$
71	70	albidv	$⊢ c = E \cap Q \to (\forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c)) \leftrightarrow \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q))))$
72	71	2albidv	$⊢ c = E \cap Q \to (\forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c)) \leftrightarrow \forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q))))$
73	64 72	anbi12d	$⊢ c = E \cap Q \to ((B \cup ran H \subseteq c \land \forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c))) \leftrightarrow (B \cup ran H \subseteq E \cap Q \land \forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q)))))$
74	63 73	elab	$⊢ E \cap Q \in \{c \| (B \cup ran H \subseteq c \land \forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c)))\} \leftrightarrow (B \cup ran H \subseteq E \cap Q \land \forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq E \cap Q \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in (E \cap Q))))$
75	26 61 74	sylanbrc	$⊢ φ \to E \cap Q \in \{c \| (B \cup ran H \subseteq c \land \forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c)))\}$
76		intss1	$⊢ E \cap Q \in \{c \| (B \cup ran H \subseteq c \land \forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c)))\} \to ⋂ \{c \| (B \cup ran H \subseteq c \land \forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c)))\} \subseteq E \cap Q$
77	75 76	syl	$⊢ φ \to ⋂ \{c \| (B \cup ran H \subseteq c \land \forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c)))\} \subseteq E \cap Q$
78	77 28	sstrdi	$⊢ φ \to ⋂ \{c \| (B \cup ran H \subseteq c \land \forall m \forall o \forall p (⟨m, o, p⟩ \in A \to \forall s \in ran L ((s [o \cup ran H] \subseteq c \land \forall x \forall y (x m y \to W (s (H (x))) \times W (s (H (y))) \subseteq K)) \to s (p) \in c)))\} \subseteq Q$
79	15 78	eqsstrd	$⊢ φ \to K C B \subseteq Q$

Metamath Proof Explorer

Theorem mclsind

Proof