Theorem mthmpps 35945

Description: Given a theorem, there is an explicitly definable witnessing provable pre-statement for the provability of the theorem. (However, this pre-statement requires infinitely many disjoint variable conditions, which is sometimes inconvenient.) (Contributed by Mario Carneiro, 18-Jul-2016.)

Hypotheses

Ref	Expression
mthmpps.r	⊢ 𝑅 = (mStRed‘𝑇)
mthmpps.j	⊢ 𝐽 = (mPPSt‘𝑇)
mthmpps.u	⊢ 𝑈 = (mThm‘𝑇)
mthmpps.d	⊢ 𝐷 = (mDV‘𝑇)
mthmpps.v	⊢ 𝑉 = (mVars‘𝑇)
mthmpps.z	⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴}))
mthmpps.m	⊢ 𝑀 = (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))

Assertion

Ref	Expression
mthmpps	⊢ (𝑇 ∈ mFS → (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 ↔ (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))))

Proof of Theorem mthmpps

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mthmpps.m	. . . . . . . 8 ⊢ 𝑀 = (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))
2		mthmpps.u	. . . . . . . . . . . . . 14 ⊢ 𝑈 = (mThm‘𝑇)
3		eqid 2765	. . . . . . . . . . . . . 14 ⊢ (mPreSt‘𝑇) = (mPreSt‘𝑇)
4	2, 3	mthmsta 35941	. . . . . . . . . . . . 13 ⊢ 𝑈 ⊆ (mPreSt‘𝑇)
5		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈)
6	4, 5	sselid 3937	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
7		mthmpps.d	. . . . . . . . . . . . 13 ⊢ 𝐷 = (mDV‘𝑇)
8		eqid 2765	. . . . . . . . . . . . 13 ⊢ (mEx‘𝑇) = (mEx‘𝑇)
9	7, 8, 3	elmpst 35899	. . . . . . . . . . . 12 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ↔ ((𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
10	6, 9	sylib 221	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ((𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
11	10	simp1d 1158	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶))
12	11	simpld 499	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐶 ⊆ 𝐷)
13		difssd 4093	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐷 ∖ (𝑍 × 𝑍)) ⊆ 𝐷)
14	12, 13	unssd 4147	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ⊆ 𝐷)
15	1, 14	eqsstrid 3977	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝑀 ⊆ 𝐷)
16	11	simprd 500	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ◡𝐶 = 𝐶)
17		cnvdif 6131	. . . . . . . . . . 11 ⊢ ◡(𝐷 ∖ (𝑍 × 𝑍)) = (◡𝐷 ∖ ◡(𝑍 × 𝑍))
18		cnvdif 6131	. . . . . . . . . . . . . 14 ⊢ ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ◡ I )
19		cnvxp 6146	. . . . . . . . . . . . . . 15 ⊢ ◡((mVR‘𝑇) × (mVR‘𝑇)) = ((mVR‘𝑇) × (mVR‘𝑇))
20		cnvi 5862	. . . . . . . . . . . . . . 15 ⊢ ◡ I = I
21	19, 20	difeq12i 4081	. . . . . . . . . . . . . 14 ⊢ (◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ◡ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
22	18, 21	eqtri 2788	. . . . . . . . . . . . 13 ⊢ ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
23		eqid 2765	. . . . . . . . . . . . . . 15 ⊢ (mVR‘𝑇) = (mVR‘𝑇)
24	23, 7	mdvval 35867	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
25	24	cnveqi 5851	. . . . . . . . . . . . 13 ⊢ ◡𝐷 = ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
26	22, 25, 24	3eqtr4i 2798	. . . . . . . . . . . 12 ⊢ ◡𝐷 = 𝐷
27		cnvxp 6146	. . . . . . . . . . . 12 ⊢ ◡(𝑍 × 𝑍) = (𝑍 × 𝑍)
28	26, 27	difeq12i 4081	. . . . . . . . . . 11 ⊢ (◡𝐷 ∖ ◡(𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍))
29	17, 28	eqtri 2788	. . . . . . . . . 10 ⊢ ◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍))
30	29	a1i 11	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍)))
31	16, 30	uneq12d 4125	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍))) = (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
32	1	cnveqi 5851	. . . . . . . . 9 ⊢ ◡𝑀 = ◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))
33		cnvun 6130	. . . . . . . . 9 ⊢ ◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) = (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍)))
34	32, 33	eqtri 2788	. . . . . . . 8 ⊢ ◡𝑀 = (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍)))
35	31, 34, 1	3eqtr4g 2825	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ◡𝑀 = 𝑀)
36	15, 35	jca 520	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀))
37	10	simp2d 1159	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin))
38	10	simp3d 1160	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐴 ∈ (mEx‘𝑇))
39	7, 8, 3	elmpst 35899	. . . . . 6 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ↔ ((𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
40	36, 37, 38, 39	syl3anbrc 1360	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
41		mthmpps.r	. . . . . . . 8 ⊢ 𝑅 = (mStRed‘𝑇)
42		mthmpps.j	. . . . . . . 8 ⊢ 𝐽 = (mPPSt‘𝑇)
43	41, 42, 2	elmthm 35939	. . . . . . 7 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 ↔ ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
44	5, 43	sylib 221	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
45		eqid 2765	. . . . . . . 8 ⊢ (mCls‘𝑇) = (mCls‘𝑇)
46		simpll 778	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑇 ∈ mFS)
47	15	adantr 485	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑀 ⊆ 𝐷)
48	37	simpld 499	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐻 ⊆ (mEx‘𝑇))
49	48	adantr 485	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐻 ⊆ (mEx‘𝑇))
50	3, 42	mppspst 35937	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐽 ⊆ (mPreSt‘𝑇)
51		simprl 782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 ∈ 𝐽)
52	50, 51	sselid 3937	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 ∈ (mPreSt‘𝑇))
53	3	mpst123 35903	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (mPreSt‘𝑇) → 𝑥 = ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩)
54	52, 53	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 = ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩)
55	54	fveq2d 6875	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘𝑥) = (𝑅‘⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩))
56		simprr 784	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
57	55, 56	eqtr3d 2802	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
58	54, 52	eqeltrrd 2866	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩ ∈ (mPreSt‘𝑇))
59		mthmpps.v	. . . . . . . . . . . . . . . . 17 ⊢ 𝑉 = (mVars‘𝑇)
60		eqid 2765	. . . . . . . . . . . . . . . . 17 ⊢ ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}))
61	59, 3, 41, 60	msrval 35901	. . . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . . 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 35901	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
65	6, 64	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
66	65	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
67	57, 62, 66	3eqtr3d 2808	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩ = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
68		fvex 6884	. . . . . . . . . . . . . . . 16 ⊢ (1st ‘(1st ‘𝑥)) ∈ V
69	68	inex1 5278	. . . . . . . . . . . . . . 15 ⊢ ((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) ∈ V
70		fvex 6884	. . . . . . . . . . . . . . 15 ⊢ (2nd ‘(1st ‘𝑥)) ∈ V
71		fvex 6884	. . . . . . . . . . . . . . 15 ⊢ (2nd ‘𝑥) ∈ V
72	69, 70, 71	otth 5457	. . . . . . . . . . . . . 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 1158	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = (𝐶 ∩ (𝑍 × 𝑍)))
75	73	simp2d 1159	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (2nd ‘(1st ‘𝑥)) = 𝐻)
76	73	simp3d 1160	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (2nd ‘𝑥) = 𝐴)
77	76	sneqd 4597	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → {(2nd ‘𝑥)} = {𝐴})
78	75, 77	uneq12d 4125	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}) = (𝐻 ∪ {𝐴}))
79	78	imaeq2d 6053	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = (𝑉 “ (𝐻 ∪ {𝐴})))
80	79	unieqd 4881	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = ∪ (𝑉 “ (𝐻 ∪ {𝐴})))
81	80, 63	eqtr4di 2818	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = 𝑍)
82	81	sqxpeqd 5684	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}))) = (𝑍 × 𝑍))
83	82	ineq2d 4175	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = ((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)))
84	74, 83	eqtr3d 2802	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝐶 ∩ (𝑍 × 𝑍)) = ((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)))
85		inss1 4191	. . . . . . . . . . 11 ⊢ (𝐶 ∩ (𝑍 × 𝑍)) ⊆ 𝐶
86	84, 85	eqsstrrdi 3984	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶)
87		eqidd 2766	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑥)))
88	87, 75, 76	oteq123d 4849	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩ = ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩)
89	54, 88	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 = ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩)
90	89, 52	eqeltrrd 2866	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
91	7, 8, 3	elmpst 35899	. . . . . . . . . . . . . 14 ⊢ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ↔ (((1st ‘(1st ‘𝑥)) ⊆ 𝐷 ∧ ◡(1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑥))) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
92	91	simp1bi 1161	. . . . . . . . . . . . 13 ⊢ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → ((1st ‘(1st ‘𝑥)) ⊆ 𝐷 ∧ ◡(1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑥))))
93	92	simpld 499	. . . . . . . . . . . 12 ⊢ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (1st ‘(1st ‘𝑥)) ⊆ 𝐷)
94	90, 93	syl 18	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1st ‘(1st ‘𝑥)) ⊆ 𝐷)
95	94	ssdifd 4101	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍)))
96		unss12 4143	. . . . . . . . . 10 ⊢ ((((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶 ∧ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍))) → (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
97	86, 95, 96	syl2anc 595	. . . . . . . . 9 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
98		inundif 4436	. . . . . . . . . 10 ⊢ (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) = (1st ‘(1st ‘𝑥))
99	98	eqcomi 2774	. . . . . . . . 9 ⊢ (1st ‘(1st ‘𝑥)) = (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)))
100	97, 99, 1	3sstr4g 3992	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1st ‘(1st ‘𝑥)) ⊆ 𝑀)
101		ssidd 3962	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐻 ⊆ 𝐻)
102	7, 8, 45, 46, 47, 49, 100, 101	ss2mcls 35931	. . . . . . 7 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥))(mCls‘𝑇)𝐻) ⊆ (𝑀(mCls‘𝑇)𝐻))
103	89, 51	eqeltrrd 2866	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ 𝐽)
104	3, 42, 45	elmpps 35936	. . . . . . . . 9 ⊢ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ 𝐽 ↔ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ∧ 𝐴 ∈ ((1st ‘(1st ‘𝑥))(mCls‘𝑇)𝐻)))
105	104	simprbi 502	. . . . . . . 8 ⊢ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ 𝐽 → 𝐴 ∈ ((1st ‘(1st ‘𝑥))(mCls‘𝑇)𝐻))
106	103, 105	syl 18	. . . . . . 7 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐴 ∈ ((1st ‘(1st ‘𝑥))(mCls‘𝑇)𝐻))
107	102, 106	sseldd 3940	. . . . . 6 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻))
108	44, 107	rexlimddv 3172	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻))
109	3, 42, 45	elmpps 35936	. . . . 5 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ↔ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ∧ 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻)))
110	40, 108, 109	sylanbrc 594	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽)
111	1	ineq1i 4171	. . . . . . . 8 ⊢ (𝑀 ∩ (𝑍 × 𝑍)) = ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍))
112		indir 4241	. . . . . . . 8 ⊢ ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍)) = ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)))
113		disjdifr 4430	. . . . . . . . . 10 ⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) = ∅
114		0ss 4357	. . . . . . . . . 10 ⊢ ∅ ⊆ (𝐶 ∩ (𝑍 × 𝑍))
115	113, 114	eqsstri 3985	. . . . . . . . 9 ⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍))
116		ssequn2 4144	. . . . . . . . 9 ⊢ (((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍)) ↔ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍)))
117	115, 116	mpbi 233	. . . . . . . 8 ⊢ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍))
118	111, 112, 117	3eqtri 2792	. . . . . . 7 ⊢ (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍))
119	118	a1i 11	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍)))
120	119	oteq1d 4846	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩ = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
121	59, 3, 41, 63	msrval 35901	. . . . . 6 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
122	40, 121	syl 18	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
123	120, 122, 65	3eqtr4d 2810	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
124	110, 123	jca 520	. . 3 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩)))
125	124	ex 417	. 2 ⊢ (𝑇 ∈ mFS → (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 → (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))))
126	41, 42, 2	mthmi 35940	. 2 ⊢ ((⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩)) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈)
127	125, 126	impbid1 228	1 ⊢ (𝑇 ∈ mFS → (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 ↔ (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ∃wrex 3089   ∖ cdif 3904   ∪ cun 3905   ∩ cin 3906   ⊆ wss 3907  ∅c0 4288  {csn 4585  ⟨cotp 4593  ∪ cuni 4868   I cid 5546   × cxp 5650  ^◡ccnv 5651   “ cima 5655  ‘cfv 6525  (class class class)co 7400  1^st c1st 7972  2^nd c2nd 7973  Fincfn 8931  mVRcmvar 35824  mExcmex 35830  mDVcmdv 35831  mVarscmvrs 35832  mPreStcmpst 35836  mStRedcmsr 35837  mFScmfs 35839  mClscmcls 35840  mPPStcmpps 35841  mThmcmthm 35842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-ot 4594  df-uni 4869  df-int 4909  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-1o 8441  df-er 8682  df-map 8814  df-pm 8815  df-en 8932  df-dom 8933  df-sdom 8934  df-fin 8935  df-card 9913  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-nn 12225  df-2 12294  df-n0 12496  df-z 12583  df-uz 12854  df-fz 13527  df-fzo 13674  df-seq 14029  df-hash 14358  df-word 14541  df-concat 14598  df-s1 14624  df-struct 17197  df-sets 17214  df-slot 17232  df-ndx 17244  df-base 17260  df-ress 17281  df-plusg 17313  df-0g 17484  df-gsum 17485  df-mgm 18688  df-sgrp 18767  df-mnd 18783  df-submnd 18832  df-frmd 18898  df-mrex 35849  df-mex 35850  df-mdv 35851  df-mrsub 35853  df-msub 35854  df-mvh 35855  df-mpst 35856  df-msr 35857  df-msta 35858  df-mfs 35859  df-mcls 35860  df-mpps 35861  df-mthm 35862

This theorem is referenced by: (None)