Metamath Proof Explorer

Theorem mclsssvlem

Description: Lemma for mclsssv . (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
mclsval.h ⊢ H = mVH ⁡ T
mclsval.a ⊢ A = mAx ⁡ T
mclsval.s ⊢ S = mSubst ⁡ T
mclsval.v ⊢ V = mVars ⁡ T
Assertion mclsssvlem ⊢ φ → ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ⊆ E

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 mclsval.h ⊢ H = mVH ⁡ T
8 mclsval.a ⊢ A = mAx ⁡ T
9 mclsval.s ⊢ S = mSubst ⁡ T
10 mclsval.v ⊢ V = mVars ⁡ T
11 eqid ⊢ mVR ⁡ T = mVR ⁡ T
12 11 2 7 mvhf ⊢ T ∈ mFS → H : mVR ⁡ T ⟶ E
13 4 12 syl ⊢ φ → H : mVR ⁡ T ⟶ E
14 13 frnd ⊢ φ → ran ⁡ H ⊆ E
15 6 14 unssd ⊢ φ → B ∪ ran ⁡ H ⊆ E
16 9 2 msubf ⊢ s ∈ ran ⁡ S → s : E ⟶ E
17 eqid ⊢ mStat ⁡ T = mStat ⁡ T
18 8 17 maxsta ⊢ T ∈ mFS → A ⊆ mStat ⁡ T
19 4 18 syl ⊢ φ → A ⊆ mStat ⁡ T
20 eqid ⊢ mPreSt ⁡ T = mPreSt ⁡ T
21 20 17 mstapst ⊢ mStat ⁡ T ⊆ mPreSt ⁡ T
22 19 21 sstrdi ⊢ φ → A ⊆ mPreSt ⁡ T
23 22 sselda ⊢ φ ∧ m o p ∈ A → m o p ∈ mPreSt ⁡ T
24 1 2 20 elmpst ⊢ m o p ∈ mPreSt ⁡ T ↔ m ⊆ D ∧ m -1 = m ∧ o ⊆ E ∧ o ∈ Fin ∧ p ∈ E
25 24 simp3bi ⊢ m o p ∈ mPreSt ⁡ T → p ∈ E
26 23 25 syl ⊢ φ ∧ m o p ∈ A → p ∈ E
27 ffvelrn ⊢ s : E ⟶ E ∧ p ∈ E → s ⁡ p ∈ E
28 16 26 27 syl2anr ⊢ φ ∧ m o p ∈ A ∧ s ∈ ran ⁡ S → s ⁡ p ∈ E
29 28 a1d ⊢ φ ∧ m o p ∈ A ∧ s ∈ ran ⁡ S → s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ E
30 29 ralrimiva ⊢ φ ∧ m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ E
31 30 ex ⊢ φ → m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ E
32 31 alrimiv ⊢ φ → ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ E
33 32 alrimivv ⊢ φ → ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ E
34 2 fvexi ⊢ E ∈ V
35 sseq2 ⊢ c = E → B ∪ ran ⁡ H ⊆ c ↔ B ∪ ran ⁡ H ⊆ E
36 sseq2 ⊢ c = E → s o ∪ ran ⁡ H ⊆ c ↔ s o ∪ ran ⁡ H ⊆ E
37 36 anbi1d ⊢ c = E → s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K ↔ s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K
38 eleq2 ⊢ c = E → s ⁡ p ∈ c ↔ s ⁡ p ∈ E
39 37 38 imbi12d ⊢ c = E → s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ E
40 39 ralbidv ⊢ c = E → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ E
41 40 imbi2d ⊢ c = E → m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ E
42 41 albidv ⊢ c = E → ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ E
43 42 2albidv ⊢ c = E → ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ E
44 35 43 anbi12d ⊢ c = E → B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ B ∪ ran ⁡ H ⊆ E ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ E
45 34 44 elab ⊢ E ∈ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ↔ B ∪ ran ⁡ H ⊆ E ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ E ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ E
46 15 33 45 sylanbrc ⊢ φ → E ∈ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c
47 intss1 ⊢ E ∈ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c → ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ⊆ E
48 46 47 syl ⊢ φ → ⋂ c | B ∪ ran ⁡ H ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ A → ∀ s ∈ ran ⁡ S s o ∪ ran ⁡ H ⊆ c ∧ ∀ x ∀ y x m y → V ⁡ s ⁡ H ⁡ x × V ⁡ s ⁡ H ⁡ y ⊆ K → s ⁡ p ∈ c ⊆ E