Theorem 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	⊢ 𝐷 = ( mDV ‘ 𝑇 )
	mclsval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	mclsval.c	⊢ 𝐶 = ( mCls ‘ 𝑇 )
	mclsval.1	⊢ ( 𝜑 → 𝑇 ∈ mFS )
	mclsval.2	⊢ ( 𝜑 → 𝐾 ⊆ 𝐷 )
	mclsval.3	⊢ ( 𝜑 → 𝐵 ⊆ 𝐸 )
	mclsax.a	⊢ 𝐴 = ( mAx ‘ 𝑇 )
	mclsax.l	⊢ 𝐿 = ( mSubst ‘ 𝑇 )
	mclsax.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mclsax.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
	mclsax.w	⊢ 𝑊 = ( mVars ‘ 𝑇 )
	mclsind.4	⊢ ( 𝜑 → 𝐵 ⊆ 𝑄 )
	mclsind.5	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑣 ) ∈ 𝑄 )
	mclsind.6	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑄 )
Assertion	mclsind	⊢ ( 𝜑 → ( 𝐾 𝐶 𝐵 ) ⊆ 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		mclsval.d	⊢ 𝐷 = ( mDV ‘ 𝑇 )
2		mclsval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
3		mclsval.c	⊢ 𝐶 = ( mCls ‘ 𝑇 )
4		mclsval.1	⊢ ( 𝜑 → 𝑇 ∈ mFS )
5		mclsval.2	⊢ ( 𝜑 → 𝐾 ⊆ 𝐷 )
6		mclsval.3	⊢ ( 𝜑 → 𝐵 ⊆ 𝐸 )
7		mclsax.a	⊢ 𝐴 = ( mAx ‘ 𝑇 )
8		mclsax.l	⊢ 𝐿 = ( mSubst ‘ 𝑇 )
9		mclsax.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
10		mclsax.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
11		mclsax.w	⊢ 𝑊 = ( mVars ‘ 𝑇 )
12		mclsind.4	⊢ ( 𝜑 → 𝐵 ⊆ 𝑄 )
13		mclsind.5	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑣 ) ∈ 𝑄 )
14		mclsind.6	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑄 )
15	1 2 3 4 5 6 10 7 8 11	mclsval	⊢ ( 𝜑 → ( 𝐾 𝐶 𝐵 ) = ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
16	6 12	ssind	⊢ ( 𝜑 → 𝐵 ⊆ ( 𝐸 ∩ 𝑄 ) )
17	9 2 10	mvhf	⊢ ( 𝑇 ∈ mFS → 𝐻 : 𝑉 ⟶ 𝐸 )
18	4 17	syl	⊢ ( 𝜑 → 𝐻 : 𝑉 ⟶ 𝐸 )
19	18	ffnd	⊢ ( 𝜑 → 𝐻 Fn 𝑉 )
20	18	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑣 ) ∈ 𝐸 )
21	20 13	elind	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑣 ) ∈ ( 𝐸 ∩ 𝑄 ) )
22	21	ralrimiva	⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝑉 ( 𝐻 ‘ 𝑣 ) ∈ ( 𝐸 ∩ 𝑄 ) )
23		ffnfv	⊢ ( 𝐻 : 𝑉 ⟶ ( 𝐸 ∩ 𝑄 ) ↔ ( 𝐻 Fn 𝑉 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐻 ‘ 𝑣 ) ∈ ( 𝐸 ∩ 𝑄 ) ) )
24	19 22 23	sylanbrc	⊢ ( 𝜑 → 𝐻 : 𝑉 ⟶ ( 𝐸 ∩ 𝑄 ) )
25	24	frnd	⊢ ( 𝜑 → ran 𝐻 ⊆ ( 𝐸 ∩ 𝑄 ) )
26	16 25	unssd	⊢ ( 𝜑 → ( 𝐵 ∪ ran 𝐻 ) ⊆ ( 𝐸 ∩ 𝑄 ) )
27		id	⊢ ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) → ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) )
28		inss2	⊢ ( 𝐸 ∩ 𝑄 ) ⊆ 𝑄
29	27 28	sstrdi	⊢ ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) → ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 )
30	4	adantr	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝑇 ∈ mFS )
31		eqid	⊢ ( mREx ‘ 𝑇 ) = ( mREx ‘ 𝑇 )
32	9 31 8 2	msubff	⊢ ( 𝑇 ∈ mFS → 𝐿 : ( ( mREx ‘ 𝑇 ) ↑pm 𝑉 ) ⟶ ( 𝐸 ↑m 𝐸 ) )
33		frn	⊢ ( 𝐿 : ( ( mREx ‘ 𝑇 ) ↑pm 𝑉 ) ⟶ ( 𝐸 ↑m 𝐸 ) → ran 𝐿 ⊆ ( 𝐸 ↑m 𝐸 ) )
34	30 32 33	3syl	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → ran 𝐿 ⊆ ( 𝐸 ↑m 𝐸 ) )
35		simpr2	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝑠 ∈ ran 𝐿 )
36	34 35	sseldd	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝑠 ∈ ( 𝐸 ↑m 𝐸 ) )
37		elmapi	⊢ ( 𝑠 ∈ ( 𝐸 ↑m 𝐸 ) → 𝑠 : 𝐸 ⟶ 𝐸 )
38	36 37	syl	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝑠 : 𝐸 ⟶ 𝐸 )
39		eqid	⊢ ( mStat ‘ 𝑇 ) = ( mStat ‘ 𝑇 )
40	7 39	maxsta	⊢ ( 𝑇 ∈ mFS → 𝐴 ⊆ ( mStat ‘ 𝑇 ) )
41	30 40	syl	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝐴 ⊆ ( mStat ‘ 𝑇 ) )
42		eqid	⊢ ( mPreSt ‘ 𝑇 ) = ( mPreSt ‘ 𝑇 )
43	42 39	mstapst	⊢ ( mStat ‘ 𝑇 ) ⊆ ( mPreSt ‘ 𝑇 )
44	41 43	sstrdi	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝐴 ⊆ ( mPreSt ‘ 𝑇 ) )
45		simpr1	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 )
46	44 45	sseldd	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mPreSt ‘ 𝑇 ) )
47	1 2 42	elmpst	⊢ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mPreSt ‘ 𝑇 ) ↔ ( ( 𝑚 ⊆ 𝐷 ∧ ◡ 𝑚 = 𝑚 ) ∧ ( 𝑜 ⊆ 𝐸 ∧ 𝑜 ∈ Fin ) ∧ 𝑝 ∈ 𝐸 ) )
48	47	simp3bi	⊢ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mPreSt ‘ 𝑇 ) → 𝑝 ∈ 𝐸 )
49	46 48	syl	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → 𝑝 ∈ 𝐸 )
50	38 49	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 )
51	50	3adant3	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝐸 )
52	51 14	elind	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) )
53	52	3exp	⊢ ( 𝜑 → ( ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ∧ 𝑠 ∈ ran 𝐿 ∧ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 ) → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) )
54	53	3expd	⊢ ( 𝜑 → ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ( 𝑠 ∈ ran 𝐿 → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) ) )
55	54	imp31	⊢ ( ( ( 𝜑 ∧ ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ) ∧ 𝑠 ∈ ran 𝐿 ) → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑄 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) )
56	29 55	syl5	⊢ ( ( ( 𝜑 ∧ ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ) ∧ 𝑠 ∈ ran 𝐿 ) → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) )
57	56	impd	⊢ ( ( ( 𝜑 ∧ ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ) ∧ 𝑠 ∈ ran 𝐿 ) → ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) )
58	57	ralrimiva	⊢ ( ( 𝜑 ∧ ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 ) → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) )
59	58	ex	⊢ ( 𝜑 → ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) )
60	59	alrimiv	⊢ ( 𝜑 → ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) )
61	60	alrimivv	⊢ ( 𝜑 → ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) )
62	2	fvexi	⊢ 𝐸 ∈ V
63	62	inex1	⊢ ( 𝐸 ∩ 𝑄 ) ∈ V
64		sseq2	⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ↔ ( 𝐵 ∪ ran 𝐻 ) ⊆ ( 𝐸 ∩ 𝑄 ) ) )
65		sseq2	⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ↔ ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ) )
66	65	anbi1d	⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ↔ ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) )
67		eleq2	⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ↔ ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) )
68	66 67	imbi12d	⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ↔ ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) )
69	68	ralbidv	⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ↔ ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) )
70	69	imbi2d	⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) )
71	70	albidv	⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) )
72	71	2albidv	⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ↔ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) )
73	64 72	anbi12d	⊢ ( 𝑐 = ( 𝐸 ∩ 𝑄 ) → ( ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ↔ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) ) )
74	63 73	elab	⊢ ( ( 𝐸 ∩ 𝑄 ) ∈ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ↔ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ ( 𝐸 ∩ 𝑄 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ ( 𝐸 ∩ 𝑄 ) ) ) ) )
75	26 61 74	sylanbrc	⊢ ( 𝜑 → ( 𝐸 ∩ 𝑄 ) ∈ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
76		intss1	⊢ ( ( 𝐸 ∩ 𝑄 ) ∈ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ ( 𝐸 ∩ 𝑄 ) )
77	75 76	syl	⊢ ( 𝜑 → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ ( 𝐸 ∩ 𝑄 ) )
78	77 28	sstrdi	⊢ ( 𝜑 → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran 𝐻 ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴 → ∀ 𝑠 ∈ ran 𝐿 ( ( ( 𝑠 “ ( 𝑜 ∪ ran 𝐻 ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑥 ) ) ) × ( 𝑊 ‘ ( 𝑠 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ 𝑄 )
79	15 78	eqsstrd	⊢ ( 𝜑 → ( 𝐾 𝐶 𝐵 ) ⊆ 𝑄 )