Step | Hyp | Ref
| Expression |
1 | | mthmpps.m |
. . . . . . . 8
⊢ 𝑀 = (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) |
2 | | mthmpps.u |
. . . . . . . . . . . . . 14
⊢ 𝑈 = (mThm‘𝑇) |
3 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(mPreSt‘𝑇) =
(mPreSt‘𝑇) |
4 | 2, 3 | mthmsta 33103 |
. . . . . . . . . . . . 13
⊢ 𝑈 ⊆ (mPreSt‘𝑇) |
5 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) |
6 | 4, 5 | sseldi 3873 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 〈𝐶, 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇)) |
7 | | mthmpps.d |
. . . . . . . . . . . . 13
⊢ 𝐷 = (mDV‘𝑇) |
8 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(mEx‘𝑇) =
(mEx‘𝑇) |
9 | 7, 8, 3 | elmpst 33061 |
. . . . . . . . . . . 12
⊢
(〈𝐶, 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) ↔ ((𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇))) |
10 | 6, 9 | sylib 221 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → ((𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇))) |
11 | 10 | simp1d 1143 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶)) |
12 | 11 | simpld 498 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 𝐶 ⊆ 𝐷) |
13 | | difssd 4021 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝐷 ∖ (𝑍 × 𝑍)) ⊆ 𝐷) |
14 | 12, 13 | unssd 4074 |
. . . . . . . 8
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ⊆ 𝐷) |
15 | 1, 14 | eqsstrid 3923 |
. . . . . . 7
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 𝑀 ⊆ 𝐷) |
16 | 11 | simprd 499 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → ◡𝐶 = 𝐶) |
17 | | cnvdif 5970 |
. . . . . . . . . . 11
⊢ ◡(𝐷 ∖ (𝑍 × 𝑍)) = (◡𝐷 ∖ ◡(𝑍 × 𝑍)) |
18 | | cnvdif 5970 |
. . . . . . . . . . . . . 14
⊢ ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ◡ I ) |
19 | | cnvxp 5983 |
. . . . . . . . . . . . . . 15
⊢ ◡((mVR‘𝑇) × (mVR‘𝑇)) = ((mVR‘𝑇) × (mVR‘𝑇)) |
20 | | cnvi 5968 |
. . . . . . . . . . . . . . 15
⊢ ◡ I = I |
21 | 19, 20 | difeq12i 4009 |
. . . . . . . . . . . . . 14
⊢ (◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ◡ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) |
22 | 18, 21 | eqtri 2761 |
. . . . . . . . . . . . 13
⊢ ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) |
23 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(mVR‘𝑇) =
(mVR‘𝑇) |
24 | 23, 7 | mdvval 33029 |
. . . . . . . . . . . . . 14
⊢ 𝐷 = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) |
25 | 24 | cnveqi 5711 |
. . . . . . . . . . . . 13
⊢ ◡𝐷 = ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) |
26 | 22, 25, 24 | 3eqtr4i 2771 |
. . . . . . . . . . . 12
⊢ ◡𝐷 = 𝐷 |
27 | | cnvxp 5983 |
. . . . . . . . . . . 12
⊢ ◡(𝑍 × 𝑍) = (𝑍 × 𝑍) |
28 | 26, 27 | difeq12i 4009 |
. . . . . . . . . . 11
⊢ (◡𝐷 ∖ ◡(𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍)) |
29 | 17, 28 | eqtri 2761 |
. . . . . . . . . 10
⊢ ◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍)) |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → ◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍))) |
31 | 16, 30 | uneq12d 4052 |
. . . . . . . 8
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍))) = (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))) |
32 | 1 | cnveqi 5711 |
. . . . . . . . 9
⊢ ◡𝑀 = ◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) |
33 | | cnvun 5969 |
. . . . . . . . 9
⊢ ◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) = (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍))) |
34 | 32, 33 | eqtri 2761 |
. . . . . . . 8
⊢ ◡𝑀 = (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍))) |
35 | 31, 34, 1 | 3eqtr4g 2798 |
. . . . . . 7
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → ◡𝑀 = 𝑀) |
36 | 15, 35 | jca 515 |
. . . . . 6
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀)) |
37 | 10 | simp2d 1144 |
. . . . . 6
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin)) |
38 | 10 | simp3d 1145 |
. . . . . 6
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 𝐴 ∈ (mEx‘𝑇)) |
39 | 7, 8, 3 | elmpst 33061 |
. . . . . 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 33101 |
. . . . . . 7
⊢
(〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈 ↔ ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)) |
44 | 5, 43 | sylib 221 |
. . . . . 6
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)) |
45 | | eqid 2738 |
. . . . . . . 8
⊢
(mCls‘𝑇) =
(mCls‘𝑇) |
46 | | simpll 767 |
. . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝑇 ∈ mFS) |
47 | 15 | adantr 484 |
. . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝑀 ⊆ 𝐷) |
48 | 37 | simpld 498 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 𝐻 ⊆ (mEx‘𝑇)) |
49 | 48 | adantr 484 |
. . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝐻 ⊆ (mEx‘𝑇)) |
50 | 3, 42 | mppspst 33099 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐽 ⊆ (mPreSt‘𝑇) |
51 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝑥 ∈ 𝐽) |
52 | 50, 51 | sseldi 3873 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝑥 ∈ (mPreSt‘𝑇)) |
53 | 3 | mpst123 33065 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (mPreSt‘𝑇) → 𝑥 = 〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝑥 = 〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉) |
55 | 54 | fveq2d 6672 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝑅‘𝑥) = (𝑅‘〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉)) |
56 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)) |
57 | 55, 56 | eqtr3d 2775 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝑅‘〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)) |
58 | 54, 52 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉 ∈
(mPreSt‘𝑇)) |
59 | | mthmpps.v |
. . . . . . . . . . . . . . . . 17
⊢ 𝑉 = (mVars‘𝑇) |
60 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) |
61 | 59, 3, 41, 60 | msrval 33063 |
. . . . . . . . . . . . . . . 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 33063 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝐶, 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) → (𝑅‘〈𝐶, 𝐻, 𝐴〉) = 〈(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
65 | 6, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝑅‘〈𝐶, 𝐻, 𝐴〉) = 〈(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
66 | 65 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝑅‘〈𝐶, 𝐻, 𝐴〉) = 〈(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
67 | 57, 62, 66 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 〈((1st
‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))), (2nd
‘(1st ‘𝑥)), (2nd ‘𝑥)〉 = 〈(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
68 | | fvex 6681 |
. . . . . . . . . . . . . . . 16
⊢
(1st ‘(1st ‘𝑥)) ∈ V |
69 | 68 | inex1 5182 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) ∈ V |
70 | | fvex 6681 |
. . . . . . . . . . . . . . 15
⊢
(2nd ‘(1st ‘𝑥)) ∈ V |
71 | | fvex 6681 |
. . . . . . . . . . . . . . 15
⊢
(2nd ‘𝑥) ∈ V |
72 | 69, 70, 71 | otth 5339 |
. . . . . . . . . . . . . 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 221 |
. . . . . . . . . . . . 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 4525 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → {(2nd
‘𝑥)} = {𝐴}) |
78 | 75, 77 | uneq12d 4052 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}) = (𝐻 ∪ {𝐴})) |
79 | 78 | imaeq2d 5897 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = (𝑉 “ (𝐻 ∪ {𝐴}))) |
80 | 79 | unieqd 4807 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = ∪ (𝑉
“ (𝐻 ∪ {𝐴}))) |
81 | 80, 63 | eqtr4di 2791 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = 𝑍) |
82 | 81 | sqxpeqd 5551 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}))) = (𝑍 × 𝑍)) |
83 | 82 | ineq2d 4101 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ((1st
‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd
‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉
“ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = ((1st
‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍))) |
84 | 74, 83 | eqtr3d 2775 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (𝐶 ∩ (𝑍 × 𝑍)) = ((1st ‘(1st
‘𝑥)) ∩ (𝑍 × 𝑍))) |
85 | | inss1 4117 |
. . . . . . . . . . 11
⊢ (𝐶 ∩ (𝑍 × 𝑍)) ⊆ 𝐶 |
86 | 84, 85 | eqsstrrdi 3930 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ((1st
‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶) |
87 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (1st
‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑥))) |
88 | 87, 75, 76 | oteq123d 4773 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 〈(1st
‘(1st ‘𝑥)), (2nd ‘(1st
‘𝑥)), (2nd
‘𝑥)〉 =
〈(1st ‘(1st ‘𝑥)), 𝐻, 𝐴〉) |
89 | 54, 88 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝑥 = 〈(1st
‘(1st ‘𝑥)), 𝐻, 𝐴〉) |
90 | 89, 52 | eqeltrrd 2834 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 〈(1st
‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇)) |
91 | 7, 8, 3 | elmpst 33061 |
. . . . . . . . . . . . . 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 498 |
. . . . . . . . . . . 12
⊢
(〈(1st ‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) → (1st
‘(1st ‘𝑥)) ⊆ 𝐷) |
94 | 90, 93 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (1st
‘(1st ‘𝑥)) ⊆ 𝐷) |
95 | 94 | ssdifd 4029 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ((1st
‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍))) |
96 | | unss12 4070 |
. . . . . . . . . 10
⊢
((((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶 ∧ ((1st
‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍))) → (((1st
‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st
‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))) |
97 | 86, 95, 96 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (((1st
‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st
‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))) |
98 | | inundif 4365 |
. . . . . . . . . 10
⊢
(((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st
‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) = (1st ‘(1st
‘𝑥)) |
99 | 98 | eqcomi 2747 |
. . . . . . . . 9
⊢
(1st ‘(1st ‘𝑥)) = (((1st ‘(1st
‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st
‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) |
100 | 97, 99, 1 | 3sstr4g 3920 |
. . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → (1st
‘(1st ‘𝑥)) ⊆ 𝑀) |
101 | | ssidd 3898 |
. . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝐻 ⊆ 𝐻) |
102 | 7, 8, 45, 46, 47, 49, 100, 101 | ss2mcls 33093 |
. . . . . . 7
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → ((1st
‘(1st ‘𝑥))(mCls‘𝑇)𝐻) ⊆ (𝑀(mCls‘𝑇)𝐻)) |
103 | 89, 51 | eqeltrrd 2834 |
. . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 〈(1st
‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ 𝐽) |
104 | 3, 42, 45 | elmpps 33098 |
. . . . . . . . 9
⊢
(〈(1st ‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ 𝐽 ↔ (〈(1st
‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) ∧ 𝐴 ∈ ((1st
‘(1st ‘𝑥))(mCls‘𝑇)𝐻))) |
105 | 104 | simprbi 500 |
. . . . . . . 8
⊢
(〈(1st ‘(1st ‘𝑥)), 𝐻, 𝐴〉 ∈ 𝐽 → 𝐴 ∈ ((1st
‘(1st ‘𝑥))(mCls‘𝑇)𝐻)) |
106 | 103, 105 | syl 17 |
. . . . . . 7
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝐴 ∈ ((1st
‘(1st ‘𝑥))(mCls‘𝑇)𝐻)) |
107 | 102, 106 | sseldd 3876 |
. . . . . 6
⊢ (((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻)) |
108 | 44, 107 | rexlimddv 3200 |
. . . . 5
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻)) |
109 | 3, 42, 45 | elmpps 33098 |
. . . . 5
⊢
(〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽 ↔ (〈𝑀, 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) ∧ 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻))) |
110 | 40, 108, 109 | sylanbrc 586 |
. . . 4
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽) |
111 | 1 | ineq1i 4097 |
. . . . . . . 8
⊢ (𝑀 ∩ (𝑍 × 𝑍)) = ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍)) |
112 | | indir 4164 |
. . . . . . . 8
⊢ ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍)) = ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) |
113 | | disjdifr 4359 |
. . . . . . . . . 10
⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) = ∅ |
114 | | 0ss 4282 |
. . . . . . . . . 10
⊢ ∅
⊆ (𝐶 ∩ (𝑍 × 𝑍)) |
115 | 113, 114 | eqsstri 3909 |
. . . . . . . . 9
⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍)) |
116 | | ssequn2 4071 |
. . . . . . . . 9
⊢ (((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍)) ↔ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍))) |
117 | 115, 116 | mpbi 233 |
. . . . . . . 8
⊢ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍)) |
118 | 111, 112,
117 | 3eqtri 2765 |
. . . . . . 7
⊢ (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍)) |
119 | 118 | a1i 11 |
. . . . . 6
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍))) |
120 | 119 | oteq1d 4770 |
. . . . 5
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → 〈(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉 = 〈(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
121 | 59, 3, 41, 63 | msrval 33063 |
. . . . . 6
⊢
(〈𝑀, 𝐻, 𝐴〉 ∈ (mPreSt‘𝑇) → (𝑅‘〈𝑀, 𝐻, 𝐴〉) = 〈(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
122 | 40, 121 | syl 17 |
. . . . 5
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝑅‘〈𝑀, 𝐻, 𝐴〉) = 〈(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴〉) |
123 | 120, 122,
65 | 3eqtr4d 2783 |
. . . 4
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (𝑅‘〈𝑀, 𝐻, 𝐴〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)) |
124 | 110, 123 | jca 515 |
. . 3
⊢ ((𝑇 ∈ mFS ∧ 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) → (〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽 ∧ (𝑅‘〈𝑀, 𝐻, 𝐴〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉))) |
125 | 124 | ex 416 |
. 2
⊢ (𝑇 ∈ mFS → (〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈 → (〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽 ∧ (𝑅‘〈𝑀, 𝐻, 𝐴〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)))) |
126 | 41, 42, 2 | mthmi 33102 |
. 2
⊢
((〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽 ∧ (𝑅‘〈𝑀, 𝐻, 𝐴〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)) → 〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈) |
127 | 125, 126 | impbid1 228 |
1
⊢ (𝑇 ∈ mFS → (〈𝐶, 𝐻, 𝐴〉 ∈ 𝑈 ↔ (〈𝑀, 𝐻, 𝐴〉 ∈ 𝐽 ∧ (𝑅‘〈𝑀, 𝐻, 𝐴〉) = (𝑅‘〈𝐶, 𝐻, 𝐴〉)))) |