| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mthmpps.m | . . . . . . . 8
⊢ 𝑀 = (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) | 
| 2 |  | mthmpps.u | . . . . . . . . . . . . . 14
⊢ 𝑈 = (mThm‘𝑇) | 
| 3 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(mPreSt‘𝑇) =
(mPreSt‘𝑇) | 
| 4 | 2, 3 | mthmsta 35583 | . . . . . . . . . . . . 13
⊢ 𝑈 ⊆ (mPreSt‘𝑇) | 
| 5 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) | 
| 6 | 4, 5 | sselid 3981 | . . . . . . . . . . . 12
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 〈𝐶, 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇)) | 
| 7 |  | mthmpps.d | . . . . . . . . . . . . 13
⊢ 𝐷 = (mDV‘𝑇) | 
| 8 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(mEx‘𝑇) =
(mEx‘𝑇) | 
| 9 | 7, 8, 3 | elmpst 35541 | . . . . . . . . . . . 12
⊢
(〈𝐶, 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) ↔ ((𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇))) | 
| 10 | 6, 9 | sylib 218 | . . . . . . . . . . 11
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → ((𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇))) | 
| 11 | 10 | simp1d 1143 | . . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶)) | 
| 12 | 11 | simpld 494 | . . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 𝐶 ⊆ 𝐷) | 
| 13 |  | difssd 4137 | . . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝐷 ∖ (𝑍 × 𝑍)) ⊆ 𝐷) | 
| 14 | 12, 13 | unssd 4192 | . . . . . . . 8
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ⊆ 𝐷) | 
| 15 | 1, 14 | eqsstrid 4022 | . . . . . . 7
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 𝑀 ⊆ 𝐷) | 
| 16 | 11 | simprd 495 | . . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → ◡𝐶 = 𝐶) | 
| 17 |  | cnvdif 6163 | . . . . . . . . . . 11
⊢ ◡(𝐷 ∖ (𝑍 × 𝑍)) = (◡𝐷 ∖ ◡(𝑍 × 𝑍)) | 
| 18 |  | cnvdif 6163 | . . . . . . . . . . . . . 14
⊢ ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ◡ I ) | 
| 19 |  | cnvxp 6177 | . . . . . . . . . . . . . . 15
⊢ ◡((mVR‘𝑇) × (mVR‘𝑇)) = ((mVR‘𝑇) × (mVR‘𝑇)) | 
| 20 |  | cnvi 6161 | . . . . . . . . . . . . . . 15
⊢ ◡ I = I | 
| 21 | 19, 20 | difeq12i 4124 | . . . . . . . . . . . . . 14
⊢ (◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ◡ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) | 
| 22 | 18, 21 | eqtri 2765 | . . . . . . . . . . . . 13
⊢ ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) | 
| 23 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢
(mVR‘𝑇) =
(mVR‘𝑇) | 
| 24 | 23, 7 | mdvval 35509 | . . . . . . . . . . . . . 14
⊢ 𝐷 = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) | 
| 25 | 24 | cnveqi 5885 | . . . . . . . . . . . . 13
⊢ ◡𝐷 = ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) | 
| 26 | 22, 25, 24 | 3eqtr4i 2775 | . . . . . . . . . . . 12
⊢ ◡𝐷 = 𝐷 | 
| 27 |  | cnvxp 6177 | . . . . . . . . . . . 12
⊢ ◡(𝑍 × 𝑍) = (𝑍 × 𝑍) | 
| 28 | 26, 27 | difeq12i 4124 | . . . . . . . . . . 11
⊢ (◡𝐷 ∖ ◡(𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍)) | 
| 29 | 17, 28 | eqtri 2765 | . . . . . . . . . 10
⊢ ◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍)) | 
| 30 | 29 | a1i 11 | . . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → ◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍))) | 
| 31 | 16, 30 | uneq12d 4169 | . . . . . . . 8
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍))) = (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))) | 
| 32 | 1 | cnveqi 5885 | . . . . . . . . 9
⊢ ◡𝑀 = ◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) | 
| 33 |  | cnvun 6162 | . . . . . . . . 9
⊢ ◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) = (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍))) | 
| 34 | 32, 33 | eqtri 2765 | . . . . . . . 8
⊢ ◡𝑀 = (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍))) | 
| 35 | 31, 34, 1 | 3eqtr4g 2802 | . . . . . . 7
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → ◡𝑀 = 𝑀) | 
| 36 | 15, 35 | jca 511 | . . . . . 6
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀)) | 
| 37 | 10 | simp2d 1144 | . . . . . 6
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin)) | 
| 38 | 10 | simp3d 1145 | . . . . . 6
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 𝐴 ∈ (mEx‘𝑇)) | 
| 39 | 7, 8, 3 | elmpst 35541 | . . . . . 6
⊢
(〈𝑀, 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) ↔ ((𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇))) | 
| 40 | 36, 37, 38, 39 | syl3anbrc 1344 | . . . . 5
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 〈𝑀, 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇)) | 
| 41 |  | mthmpps.r | . . . . . . . 8
⊢ 𝑅 = (mStRed‘𝑇) | 
| 42 |  | mthmpps.j | . . . . . . . 8
⊢ 𝐽 = (mPPSt‘𝑇) | 
| 43 | 41, 42, 2 | elmthm 35581 | . . . . . . 7
⊢
(〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈 ↔ ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)) | 
| 44 | 5, 43 | sylib 218 | . . . . . 6
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)) | 
| 45 |  | eqid 2737 | . . . . . . . 8
⊢
(mCls‘𝑇) =
(mCls‘𝑇) | 
| 46 |  | simpll 767 | . . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝑇 ∈ mFS) | 
| 47 | 15 | adantr 480 | . . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝑀 ⊆ 𝐷) | 
| 48 | 37 | simpld 494 | . . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 𝐻 ⊆ (mEx‘𝑇)) | 
| 49 | 48 | adantr 480 | . . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝐻 ⊆ (mEx‘𝑇)) | 
| 50 | 3, 42 | mppspst 35579 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐽 ⊆ (mPreSt‘𝑇) | 
| 51 |  | simprl 771 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝑥 ∈ 𝐽) | 
| 52 | 50, 51 | sselid 3981 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝑥 ∈ (mPreSt‘𝑇)) | 
| 53 | 3 | mpst123 35545 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (mPreSt‘𝑇) → 𝑥 = 〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉) | 
| 54 | 52, 53 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝑥 = 〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉) | 
| 55 | 54 | fveq2d 6910 | . . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝑅‘𝑥) = (𝑅‘〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉)) | 
| 56 |  | simprr 773 | . . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)) | 
| 57 | 55, 56 | eqtr3d 2779 | . . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝑅‘〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)) | 
| 58 | 54, 52 | eqeltrrd 2842 | . . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉 ∈
(mPreSt‘𝑇)) | 
| 59 |  | mthmpps.v | . . . . . . . . . . . . . . . . 17
⊢ 𝑉 = (mVars‘𝑇) | 
| 60 |  | eqid 2737 | . . . . . . . . . . . . . . . . 17
⊢ ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) | 
| 61 | 59, 3, 41, 60 | msrval 35543 | . . . . . . . . . . . . . . . 16
⊢
(〈(1st ‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉 ∈
(mPreSt‘𝑇) →
(𝑅‘〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉) =
〈((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))), (2nd
‘(1st ‘𝑥)), (2nd ‘𝑥)〉) | 
| 62 | 58, 61 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝑅‘〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉) =
〈((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))), (2nd
‘(1st ‘𝑥)), (2nd ‘𝑥)〉) | 
| 63 |  | mthmpps.z | . . . . . . . . . . . . . . . . . 18
⊢ 𝑍 = ∪
(𝑉 “ (𝐻 ∪ {𝐴})) | 
| 64 | 59, 3, 41, 63 | msrval 35543 | . . . . . . . . . . . . . . . . 17
⊢
(〈𝐶, 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) → (𝑅‘〈𝐶, 𝐻, 𝐴〉) = 〈(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) | 
| 65 | 6, 64 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝑅‘〈𝐶, 𝐻, 𝐴〉) = 〈(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) | 
| 66 | 65 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝑅‘〈𝐶, 𝐻, 𝐴〉) = 〈(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) | 
| 67 | 57, 62, 66 | 3eqtr3d 2785 | . . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 〈((1st
‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))), (2nd
‘(1st ‘𝑥)), (2nd ‘𝑥)〉 = 〈(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) | 
| 68 |  | fvex 6919 | . . . . . . . . . . . . . . . 16
⊢
(1st ‘(1st ‘𝑥)) ∈ V | 
| 69 | 68 | inex1 5317 | . . . . . . . . . . . . . . 15
⊢
((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) ∈ V | 
| 70 |  | fvex 6919 | . . . . . . . . . . . . . . 15
⊢
(2nd ‘(1st ‘𝑥)) ∈ V | 
| 71 |  | fvex 6919 | . . . . . . . . . . . . . . 15
⊢
(2nd ‘𝑥) ∈ V | 
| 72 | 69, 70, 71 | otth 5489 | . . . . . . . . . . . . . 14
⊢
(〈((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))), (2nd
‘(1st ‘𝑥)), (2nd ‘𝑥)〉 = 〈(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉 ↔ (((1st
‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = (𝐶 ∩ (𝑍 × 𝑍)) ∧ (2nd
‘(1st ‘𝑥)) = 𝐻 ∧ (2nd ‘𝑥) = 𝐴)) | 
| 73 | 67, 72 | sylib 218 | . . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (((1st
‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = (𝐶 ∩ (𝑍 × 𝑍)) ∧ (2nd
‘(1st ‘𝑥)) = 𝐻 ∧ (2nd ‘𝑥) = 𝐴)) | 
| 74 | 73 | simp1d 1143 | . . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ((1st
‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = (𝐶 ∩ (𝑍 × 𝑍))) | 
| 75 | 73 | simp2d 1144 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (2nd
‘(1st ‘𝑥)) = 𝐻) | 
| 76 | 73 | simp3d 1145 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (2nd
‘𝑥) = 𝐴) | 
| 77 | 76 | sneqd 4638 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → {(2nd
‘𝑥)} = {𝐴}) | 
| 78 | 75, 77 | uneq12d 4169 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}) = (𝐻 ∪ {𝐴})) | 
| 79 | 78 | imaeq2d 6078 | . . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = (𝑉 “ (𝐻 ∪ {𝐴}))) | 
| 80 | 79 | unieqd 4920 | . . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = ∪ (𝑉
“ (𝐻 ∪ {𝐴}))) | 
| 81 | 80, 63 | eqtr4di 2795 | . . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = 𝑍) | 
| 82 | 81 | sqxpeqd 5717 | . . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}))) = (𝑍 × 𝑍)) | 
| 83 | 82 | ineq2d 4220 | . . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ((1st
‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = ((1st
‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍))) | 
| 84 | 74, 83 | eqtr3d 2779 | . . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝐶 ∩ (𝑍 × 𝑍)) = ((1st ‘(1st
‘𝑥)) ∩ (𝑍 × 𝑍))) | 
| 85 |  | inss1 4237 | . . . . . . . . . . 11
⊢ (𝐶 ∩ (𝑍 × 𝑍)) ⊆ 𝐶 | 
| 86 | 84, 85 | eqsstrrdi 4029 | . . . . . . . . . 10
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ((1st
‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶) | 
| 87 |  | eqidd 2738 | . . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (1st
‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑥))) | 
| 88 | 87, 75, 76 | oteq123d 4888 | . . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉 =
〈(1st ‘(1st ‘𝑥)), 𝐻, 𝐴〉) | 
| 89 | 54, 88 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝑥 = 〈(1st
‘(1st ‘𝑥)), 𝐻, 𝐴〉) | 
| 90 | 89, 52 | eqeltrrd 2842 | . . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 〈(1st
‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇)) | 
| 91 | 7, 8, 3 | elmpst 35541 | . . . . . . . . . . . . . 14
⊢
(〈(1st ‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) ↔ (((1st
‘(1st ‘𝑥)) ⊆ 𝐷 ∧ ◡(1st ‘(1st
‘𝑥)) =
(1st ‘(1st ‘𝑥))) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇))) | 
| 92 | 91 | simp1bi 1146 | . . . . . . . . . . . . 13
⊢
(〈(1st ‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) → ((1st
‘(1st ‘𝑥)) ⊆ 𝐷 ∧ ◡(1st ‘(1st
‘𝑥)) =
(1st ‘(1st ‘𝑥)))) | 
| 93 | 92 | simpld 494 | . . . . . . . . . . . 12
⊢
(〈(1st ‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) → (1st
‘(1st ‘𝑥)) ⊆ 𝐷) | 
| 94 | 90, 93 | syl 17 | . . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (1st
‘(1st ‘𝑥)) ⊆ 𝐷) | 
| 95 | 94 | ssdifd 4145 | . . . . . . . . . 10
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ((1st
‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍))) | 
| 96 |  | unss12 4188 | . . . . . . . . . 10
⊢
((((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶 ∧ ((1st
‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍))) → (((1st
‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st
‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))) | 
| 97 | 86, 95, 96 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (((1st
‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st
‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))) | 
| 98 |  | inundif 4479 | . . . . . . . . . 10
⊢
(((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st
‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) = (1st ‘(1st
‘𝑥)) | 
| 99 | 98 | eqcomi 2746 | . . . . . . . . 9
⊢
(1st ‘(1st ‘𝑥)) = (((1st ‘(1st
‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st
‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) | 
| 100 | 97, 99, 1 | 3sstr4g 4037 | . . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (1st
‘(1st ‘𝑥)) ⊆ 𝑀) | 
| 101 |  | ssidd 4007 | . . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝐻 ⊆ 𝐻) | 
| 102 | 7, 8, 45, 46, 47, 49, 100, 101 | ss2mcls 35573 | . . . . . . 7
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ((1st
‘(1st ‘𝑥))(mCls‘𝑇)𝐻) ⊆ (𝑀(mCls‘𝑇)𝐻)) | 
| 103 | 89, 51 | eqeltrrd 2842 | . . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 〈(1st
‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ 𝐽) | 
| 104 | 3, 42, 45 | elmpps 35578 | . . . . . . . . 9
⊢
(〈(1st ‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ 𝐽 ↔ (〈(1st
‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) ∧ 𝐴 ∈ ((1st
‘(1st ‘𝑥))(mCls‘𝑇)𝐻))) | 
| 105 | 104 | simprbi 496 | . . . . . . . 8
⊢
(〈(1st ‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ 𝐽 → 𝐴 ∈ ((1st
‘(1st ‘𝑥))(mCls‘𝑇)𝐻)) | 
| 106 | 103, 105 | syl 17 | . . . . . . 7
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝐴 ∈ ((1st
‘(1st ‘𝑥))(mCls‘𝑇)𝐻)) | 
| 107 | 102, 106 | sseldd 3984 | . . . . . 6
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻)) | 
| 108 | 44, 107 | rexlimddv 3161 | . . . . 5
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻)) | 
| 109 | 3, 42, 45 | elmpps 35578 | . . . . 5
⊢
(〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽 ↔ (〈𝑀, 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) ∧ 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻))) | 
| 110 | 40, 108, 109 | sylanbrc 583 | . . . 4
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽) | 
| 111 | 1 | ineq1i 4216 | . . . . . . . 8
⊢ (𝑀 ∩ (𝑍 × 𝑍)) = ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍)) | 
| 112 |  | indir 4286 | . . . . . . . 8
⊢ ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍)) = ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) | 
| 113 |  | disjdifr 4473 | . . . . . . . . . 10
⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) = ∅ | 
| 114 |  | 0ss 4400 | . . . . . . . . . 10
⊢ ∅
⊆ (𝐶 ∩ (𝑍 × 𝑍)) | 
| 115 | 113, 114 | eqsstri 4030 | . . . . . . . . 9
⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍)) | 
| 116 |  | ssequn2 4189 | . . . . . . . . 9
⊢ (((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍)) ↔ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍))) | 
| 117 | 115, 116 | mpbi 230 | . . . . . . . 8
⊢ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍)) | 
| 118 | 111, 112,
117 | 3eqtri 2769 | . . . . . . 7
⊢ (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍)) | 
| 119 | 118 | a1i 11 | . . . . . 6
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍))) | 
| 120 | 119 | oteq1d 4885 | . . . . 5
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 〈(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉 = 〈(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) | 
| 121 | 59, 3, 41, 63 | msrval 35543 | . . . . . 6
⊢
(〈𝑀, 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) → (𝑅‘〈𝑀, 𝐻, 𝐴〉) = 〈(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) | 
| 122 | 40, 121 | syl 17 | . . . . 5
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝑅‘〈𝑀, 𝐻, 𝐴〉) = 〈(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) | 
| 123 | 120, 122,
65 | 3eqtr4d 2787 | . . . 4
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝑅‘〈𝑀, 𝐻, 𝐴〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)) | 
| 124 | 110, 123 | jca 511 | . . 3
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽 ∧ (𝑅‘〈𝑀, 𝐻, 𝐴〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) | 
| 125 | 124 | ex 412 | . 2
⊢ (𝑇 ∈ mFS → (〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈 → (〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽 ∧ (𝑅‘〈𝑀, 𝐻, 𝐴〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)))) | 
| 126 | 41, 42, 2 | mthmi 35582 | . 2
⊢
((〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽 ∧ (𝑅‘〈𝑀, 𝐻, 𝐴〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)) → 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) | 
| 127 | 125, 126 | impbid1 225 | 1
⊢ (𝑇 ∈ mFS → (〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈 ↔ (〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽 ∧ (𝑅‘〈𝑀, 𝐻, 𝐴〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)))) |