Metamath Proof Explorer

Theorem mclsax

Description: The closure is closed under axiom application. (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 ⊢ φ → T ∈ mFS
mclsval.2 ⊢ φ → K ⊆ D
mclsval.3 ⊢ φ → B ⊆ 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
mclsax.4 ⊢ φ → M O P ∈ A
mclsax.5 ⊢ φ → S ∈ ran ⁡ L
mclsax.6 ⊢ φ ∧ x ∈ O → S ⁡ x ∈ K C B
mclsax.7 ⊢ φ ∧ v ∈ V → S ⁡ H ⁡ v ∈ K C B
mclsax.8 ⊢ φ ∧ x M y ∧ a ∈ W ⁡ S ⁡ H ⁡ x ∧ b ∈ W ⁡ S ⁡ H ⁡ y → a K b
Assertion mclsax ⊢ φ → S ⁡ P ∈ K C B

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 ⊢ φ → T ∈ mFS
5 mclsval.2 ⊢ φ → K ⊆ D
6 mclsval.3 ⊢ φ → B ⊆ 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 mclsax.4 ⊢ φ → M O P ∈ A
13 mclsax.5 ⊢ φ → S ∈ ran ⁡ L
14 mclsax.6 ⊢ φ ∧ x ∈ O → S ⁡ x ∈ K C B
15 mclsax.7 ⊢ φ ∧ v ∈ V → S ⁡ H ⁡ v ∈ K C B
16 mclsax.8 ⊢ φ ∧ x M y ∧ a ∈ W ⁡ S ⁡ H ⁡ x ∧ b ∈ W ⁡ S ⁡ H ⁡ y → a K b
17 abid ⊢ c ∈ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
18 intss1 ⊢ c ∈ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ⊆ c
19 17 18 sylbir ⊢ B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ⊆ c
20 1 2 3 4 5 6 10 7 8 11 mclsval ⊢ φ → K C B = ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
21 20 sseq1d ⊢ φ → K C B ⊆ c ↔ ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ⊆ c
22 19 21 syl5ibr ⊢ φ → B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → K C B ⊆ c
23 sstr2 ⊢ s o ∪ ran ⁡ H ⊆ K C B → K C B ⊆ c → s o ∪ ran ⁡ H ⊆ c
24 23 com12 ⊢ K C B ⊆ c → s o ∪ ran ⁡ H ⊆ K C B → s o ∪ ran ⁡ H ⊆ c
25 24 anim1d ⊢ K C B ⊆ c → s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K
26 25 imim1d ⊢ K C B ⊆ c → s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
27 26 ralimdv ⊢ K C B ⊆ c → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
28 27 imim2d ⊢ K C B ⊆ c → m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
29 28 alimdv ⊢ K C B ⊆ c → ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
30 29 2alimdv ⊢ K C B ⊆ c → ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
31 30 com12 ⊢ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → K C B ⊆ c → ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
32 31 adantl ⊢ B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → K C B ⊆ c → ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
33 22 32 sylcom ⊢ φ → B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
34 eqid ⊢ mPreSt ⁡ T = mPreSt ⁡ T
35 eqid ⊢ mStat ⁡ T = mStat ⁡ T
36 34 35 mstapst ⊢ mStat ⁡ T ⊆ mPreSt ⁡ T
37 7 35 maxsta ⊢ T ∈ mFS → A ⊆ mStat ⁡ T
38 4 37 syl ⊢ φ → A ⊆ mStat ⁡ T
39 38 12 sseldd ⊢ φ → M O P ∈ mStat ⁡ T
40 36 39 sseldi ⊢ φ → M O P ∈ mPreSt ⁡ T
41 34 mpstrcl ⊢ M O P ∈ mPreSt ⁡ T → M ∈ V ∧ O ∈ V ∧ P ∈ V
42 simp1 ⊢ m = M ∧ o = O ∧ p = P → m = M
43 simp2 ⊢ m = M ∧ o = O ∧ p = P → o = O
44 simp3 ⊢ m = M ∧ o = O ∧ p = P → p = P
45 42 43 44 oteq123d ⊢ m = M ∧ o = O ∧ p = P → m o p = M O P
46 45 eleq1d ⊢ m = M ∧ o = O ∧ p = P → m o p ∈ A ↔ M O P ∈ A
47 43 uneq1d ⊢ m = M ∧ o = O ∧ p = P → o ∪ ran ⁡ H = O ∪ ran ⁡ H
48 47 imaeq2d ⊢ m = M ∧ o = O ∧ p = P → s o ∪ ran ⁡ H = s O ∪ ran ⁡ H
49 48 sseq1d ⊢ m = M ∧ o = O ∧ p = P → s o ∪ ran ⁡ H ⊆ K C B ↔ s O ∪ ran ⁡ H ⊆ K C B
50 42 breqd ⊢ m = M ∧ o = O ∧ p = P → x m y ↔ x M y
51 50 imbi1d ⊢ m = M ∧ o = O ∧ p = P → x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K ↔ x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K
52 51 2albidv ⊢ m = M ∧ o = O ∧ p = P → ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K ↔ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K
53 49 52 anbi12d ⊢ m = M ∧ o = O ∧ p = P → s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K ↔ s O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K
54 44 fveq2d ⊢ m = M ∧ o = O ∧ p = P → s ⁡ p = s ⁡ P
55 54 eleq1d ⊢ m = M ∧ o = O ∧ p = P → s ⁡ p ∈ c ↔ s ⁡ P ∈ c
56 53 55 imbi12d ⊢ m = M ∧ o = O ∧ p = P → s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ s O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ P ∈ c
57 56 ralbidv ⊢ m = M ∧ o = O ∧ p = P → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ ∀ s ∈ ran ⁡ L s O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ P ∈ c
58 46 57 imbi12d ⊢ m = M ∧ o = O ∧ p = P → m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ M O P ∈ A → ∀ s ∈ ran ⁡ L s O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ P ∈ c
59 58 spc3gv ⊢ M ∈ V ∧ O ∈ V ∧ P ∈ V → ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → M O P ∈ A → ∀ s ∈ ran ⁡ L s O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ P ∈ c
60 40 41 59 3syl ⊢ φ → ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → M O P ∈ A → ∀ s ∈ ran ⁡ L s O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ P ∈ c
61 elun ⊢ x ∈ O ∪ ran ⁡ H ↔ x ∈ O ∨ x ∈ ran ⁡ H
62 15 ralrimiva ⊢ φ → ∀ v ∈ V S ⁡ H ⁡ v ∈ K C B
63 9 2 10 mvhf ⊢ T ∈ mFS → H : V ⟶ E
64 4 63 syl ⊢ φ → H : V ⟶ E
65 ffn ⊢ H : V ⟶ E → H Fn V
66 fveq2 ⊢ x = H ⁡ v → S ⁡ x = S ⁡ H ⁡ v
67 66 eleq1d ⊢ x = H ⁡ v → S ⁡ x ∈ K C B ↔ S ⁡ H ⁡ v ∈ K C B
68 67 ralrn ⊢ H Fn V → ∀ x ∈ ran ⁡ H S ⁡ x ∈ K C B ↔ ∀ v ∈ V S ⁡ H ⁡ v ∈ K C B
69 64 65 68 3syl ⊢ φ → ∀ x ∈ ran ⁡ H S ⁡ x ∈ K C B ↔ ∀ v ∈ V S ⁡ H ⁡ v ∈ K C B
70 62 69 mpbird ⊢ φ → ∀ x ∈ ran ⁡ H S ⁡ x ∈ K C B
71 70 r19.21bi ⊢ φ ∧ x ∈ ran ⁡ H → S ⁡ x ∈ K C B
72 14 71 jaodan ⊢ φ ∧ x ∈ O ∨ x ∈ ran ⁡ H → S ⁡ x ∈ K C B
73 61 72 sylan2b ⊢ φ ∧ x ∈ O ∪ ran ⁡ H → S ⁡ x ∈ K C B
74 73 ralrimiva ⊢ φ → ∀ x ∈ O ∪ ran ⁡ H S ⁡ x ∈ K C B
75 8 2 msubf ⊢ S ∈ ran ⁡ L → S : E ⟶ E
76 13 75 syl ⊢ φ → S : E ⟶ E
77 76 ffund ⊢ φ → Fun ⁡ S
78 1 2 34 elmpst ⊢ M O P ∈ mPreSt ⁡ T ↔ M ⊆ D ∧ M -1 = M ∧ O ⊆ E ∧ O ∈ Fin ∧ P ∈ E
79 40 78 sylib ⊢ φ → M ⊆ D ∧ M -1 = M ∧ O ⊆ E ∧ O ∈ Fin ∧ P ∈ E
80 79 simp2d ⊢ φ → O ⊆ E ∧ O ∈ Fin
81 80 simpld ⊢ φ → O ⊆ E
82 76 fdmd ⊢ φ → dom ⁡ S = E
83 81 82 sseqtrrd ⊢ φ → O ⊆ dom ⁡ S
84 64 frnd ⊢ φ → ran ⁡ H ⊆ E
85 84 82 sseqtrrd ⊢ φ → ran ⁡ H ⊆ dom ⁡ S
86 83 85 unssd ⊢ φ → O ∪ ran ⁡ H ⊆ dom ⁡ S
87 funimass4 ⊢ Fun ⁡ S ∧ O ∪ ran ⁡ H ⊆ dom ⁡ S → S O ∪ ran ⁡ H ⊆ K C B ↔ ∀ x ∈ O ∪ ran ⁡ H S ⁡ x ∈ K C B
88 77 86 87 syl2anc ⊢ φ → S O ∪ ran ⁡ H ⊆ K C B ↔ ∀ x ∈ O ∪ ran ⁡ H S ⁡ x ∈ K C B
89 74 88 mpbird ⊢ φ → S O ∪ ran ⁡ H ⊆ K C B
90 16 3exp2 ⊢ φ → x M y → a ∈ W ⁡ S ⁡ H ⁡ x → b ∈ W ⁡ S ⁡ H ⁡ y → a K b
91 90 imp4b ⊢ φ ∧ x M y → a ∈ W ⁡ S ⁡ H ⁡ x ∧ b ∈ W ⁡ S ⁡ H ⁡ y → a K b
92 91 ralrimivv ⊢ φ ∧ x M y → ∀ a ∈ W ⁡ S ⁡ H ⁡ x ∀ b ∈ W ⁡ S ⁡ H ⁡ y a K b
93 dfss3 ⊢ W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K ↔ ∀ z ∈ W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y z ∈ K
94 eleq1 ⊢ z = a b → z ∈ K ↔ a b ∈ K
95 df-br ⊢ a K b ↔ a b ∈ K
96 94 95 syl6bbr ⊢ z = a b → z ∈ K ↔ a K b
97 96 ralxp ⊢ ∀ z ∈ W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y z ∈ K ↔ ∀ a ∈ W ⁡ S ⁡ H ⁡ x ∀ b ∈ W ⁡ S ⁡ H ⁡ y a K b
98 93 97 bitri ⊢ W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K ↔ ∀ a ∈ W ⁡ S ⁡ H ⁡ x ∀ b ∈ W ⁡ S ⁡ H ⁡ y a K b
99 92 98 sylibr ⊢ φ ∧ x M y → W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K
100 99 ex ⊢ φ → x M y → W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K
101 100 alrimivv ⊢ φ → ∀ x ∀ y x M y → W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K
102 89 101 jca ⊢ φ → S O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K
103 imaeq1 ⊢ s = S → s O ∪ ran ⁡ H = S O ∪ ran ⁡ H
104 103 sseq1d ⊢ s = S → s O ∪ ran ⁡ H ⊆ K C B ↔ S O ∪ ran ⁡ H ⊆ K C B
105 fveq1 ⊢ s = S → s ⁡ H ⁡ x = S ⁡ H ⁡ x
106 105 fveq2d ⊢ s = S → W ⁡ s ⁡ H ⁡ x = W ⁡ S ⁡ H ⁡ x
107 fveq1 ⊢ s = S → s ⁡ H ⁡ y = S ⁡ H ⁡ y
108 107 fveq2d ⊢ s = S → W ⁡ s ⁡ H ⁡ y = W ⁡ S ⁡ H ⁡ y
109 106 108 xpeq12d ⊢ s = S → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y = W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y
110 109 sseq1d ⊢ s = S → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K ↔ W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K
111 110 imbi2d ⊢ s = S → x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K ↔ x M y → W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K
112 111 2albidv ⊢ s = S → ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K ↔ ∀ x ∀ y x M y → W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K
113 104 112 anbi12d ⊢ s = S → s O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K ↔ S O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K
114 fveq1 ⊢ s = S → s ⁡ P = S ⁡ P
115 114 eleq1d ⊢ s = S → s ⁡ P ∈ c ↔ S ⁡ P ∈ c
116 113 115 imbi12d ⊢ s = S → s O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ P ∈ c ↔ S O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K → S ⁡ P ∈ c
117 116 rspcv ⊢ S ∈ ran ⁡ L → ∀ s ∈ ran ⁡ L s O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ P ∈ c → S O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K → S ⁡ P ∈ c
118 13 117 syl ⊢ φ → ∀ s ∈ ran ⁡ L s O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ P ∈ c → S O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ S ⁡ H ⁡ x × W ⁡ S ⁡ H ⁡ y ⊆ K → S ⁡ P ∈ c
119 102 118 mpid ⊢ φ → ∀ s ∈ ran ⁡ L s O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ P ∈ c → S ⁡ P ∈ c
120 12 119 embantd ⊢ φ → M O P ∈ A → ∀ s ∈ ran ⁡ L s O ∪ ran ⁡ H ⊆ K C B ∧ ∀ x ∀ y x M y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ P ∈ c → S ⁡ P ∈ c
121 33 60 120 3syld ⊢ φ → B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → S ⁡ P ∈ c
122 121 alrimiv ⊢ φ → ∀ c B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → S ⁡ P ∈ c
123 fvex ⊢ S ⁡ P ∈ V
124 123 elintab ⊢ S ⁡ P ∈ ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ ∀ c B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → S ⁡ P ∈ c
125 122 124 sylibr ⊢ φ → S ⁡ P ∈ ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ L s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → W ⁡ s ⁡ H ⁡ x × W ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
126 125 20 eleqtrrd ⊢ φ → S ⁡ P ∈ K C B