Metamath Proof Explorer


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 ffvelrnda ( ( 𝜑𝑣𝑉 ) → ( 𝐻𝑣 ) ∈ 𝐸 )
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 ffvelrnd ( ( 𝜑 ∧ ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ 𝐴𝑠 ∈ 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 ( 𝜑 → ( 𝐾 𝐶 𝐵 ) ⊆ 𝑄 )