Theorem mthmpps 35776

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 2736	. . . . . . . . . . . . . 14 ⊢ (mPreSt‘𝑇) = (mPreSt‘𝑇)
4	2, 3	mthmsta 35772	. . . . . . . . . . . . 13 ⊢ 𝑈 ⊆ (mPreSt‘𝑇)
5		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈)
6	4, 5	sselid 3931	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
7		mthmpps.d	. . . . . . . . . . . . 13 ⊢ 𝐷 = (mDV‘𝑇)
8		eqid 2736	. . . . . . . . . . . . 13 ⊢ (mEx‘𝑇) = (mEx‘𝑇)
9	7, 8, 3	elmpst 35730	. . . . . . . . . . . 12 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ↔ ((𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
10	6, 9	sylib 218	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ((𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
11	10	simp1d 1142	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶))
12	11	simpld 494	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐶 ⊆ 𝐷)
13		difssd 4089	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐷 ∖ (𝑍 × 𝑍)) ⊆ 𝐷)
14	12, 13	unssd 4144	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ⊆ 𝐷)
15	1, 14	eqsstrid 3972	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝑀 ⊆ 𝐷)
16	11	simprd 495	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ◡𝐶 = 𝐶)
17		cnvdif 6101	. . . . . . . . . . 11 ⊢ ◡(𝐷 ∖ (𝑍 × 𝑍)) = (◡𝐷 ∖ ◡(𝑍 × 𝑍))
18		cnvdif 6101	. . . . . . . . . . . . . 14 ⊢ ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ◡ I )
19		cnvxp 6115	. . . . . . . . . . . . . . 15 ⊢ ◡((mVR‘𝑇) × (mVR‘𝑇)) = ((mVR‘𝑇) × (mVR‘𝑇))
20		cnvi 6099	. . . . . . . . . . . . . . 15 ⊢ ◡ I = I
21	19, 20	difeq12i 4076	. . . . . . . . . . . . . 14 ⊢ (◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ◡ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
22	18, 21	eqtri 2759	. . . . . . . . . . . . 13 ⊢ ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
23		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (mVR‘𝑇) = (mVR‘𝑇)
24	23, 7	mdvval 35698	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
25	24	cnveqi 5823	. . . . . . . . . . . . 13 ⊢ ◡𝐷 = ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
26	22, 25, 24	3eqtr4i 2769	. . . . . . . . . . . 12 ⊢ ◡𝐷 = 𝐷
27		cnvxp 6115	. . . . . . . . . . . 12 ⊢ ◡(𝑍 × 𝑍) = (𝑍 × 𝑍)
28	26, 27	difeq12i 4076	. . . . . . . . . . 11 ⊢ (◡𝐷 ∖ ◡(𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍))
29	17, 28	eqtri 2759	. . . . . . . . . 10 ⊢ ◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍))
30	29	a1i 11	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍)))
31	16, 30	uneq12d 4121	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍))) = (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
32	1	cnveqi 5823	. . . . . . . . 9 ⊢ ◡𝑀 = ◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))
33		cnvun 6100	. . . . . . . . 9 ⊢ ◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) = (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍)))
34	32, 33	eqtri 2759	. . . . . . . 8 ⊢ ◡𝑀 = (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍)))
35	31, 34, 1	3eqtr4g 2796	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ◡𝑀 = 𝑀)
36	15, 35	jca 511	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀))
37	10	simp2d 1143	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin))
38	10	simp3d 1144	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐴 ∈ (mEx‘𝑇))
39	7, 8, 3	elmpst 35730	. . . . . 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 35770	. . . . . . 7 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 ↔ ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
44	5, 43	sylib 218	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
45		eqid 2736	. . . . . . . 8 ⊢ (mCls‘𝑇) = (mCls‘𝑇)
46		simpll 766	. . . . . . . 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 35768	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐽 ⊆ (mPreSt‘𝑇)
51		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 ∈ 𝐽)
52	50, 51	sselid 3931	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 ∈ (mPreSt‘𝑇))
53	3	mpst123 35734	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (mPreSt‘𝑇) → 𝑥 = ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩)
54	52, 53	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 = ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩)
55	54	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘𝑥) = (𝑅‘⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩))
56		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
57	55, 56	eqtr3d 2773	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
58	54, 52	eqeltrrd 2837	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩ ∈ (mPreSt‘𝑇))
59		mthmpps.v	. . . . . . . . . . . . . . . . 17 ⊢ 𝑉 = (mVars‘𝑇)
60		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}))
61	59, 3, 41, 60	msrval 35732	. . . . . . . . . . . . . . . 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 35732	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
65	6, 64	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
66	65	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
67	57, 62, 66	3eqtr3d 2779	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩ = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
68		fvex 6847	. . . . . . . . . . . . . . . 16 ⊢ (1st ‘(1st ‘𝑥)) ∈ V
69	68	inex1 5262	. . . . . . . . . . . . . . 15 ⊢ ((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) ∈ V
70		fvex 6847	. . . . . . . . . . . . . . 15 ⊢ (2nd ‘(1st ‘𝑥)) ∈ V
71		fvex 6847	. . . . . . . . . . . . . . 15 ⊢ (2nd ‘𝑥) ∈ V
72	69, 70, 71	otth 5432	. . . . . . . . . . . . . 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 1142	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = (𝐶 ∩ (𝑍 × 𝑍)))
75	73	simp2d 1143	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (2nd ‘(1st ‘𝑥)) = 𝐻)
76	73	simp3d 1144	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (2nd ‘𝑥) = 𝐴)
77	76	sneqd 4592	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → {(2nd ‘𝑥)} = {𝐴})
78	75, 77	uneq12d 4121	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}) = (𝐻 ∪ {𝐴}))
79	78	imaeq2d 6019	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = (𝑉 “ (𝐻 ∪ {𝐴})))
80	79	unieqd 4876	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = ∪ (𝑉 “ (𝐻 ∪ {𝐴})))
81	80, 63	eqtr4di 2789	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = 𝑍)
82	81	sqxpeqd 5656	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}))) = (𝑍 × 𝑍))
83	82	ineq2d 4172	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = ((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)))
84	74, 83	eqtr3d 2773	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝐶 ∩ (𝑍 × 𝑍)) = ((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)))
85		inss1 4189	. . . . . . . . . . 11 ⊢ (𝐶 ∩ (𝑍 × 𝑍)) ⊆ 𝐶
86	84, 85	eqsstrrdi 3979	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶)
87		eqidd 2737	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑥)))
88	87, 75, 76	oteq123d 4844	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩ = ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩)
89	54, 88	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 = ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩)
90	89, 52	eqeltrrd 2837	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
91	7, 8, 3	elmpst 35730	. . . . . . . . . . . . . 14 ⊢ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ↔ (((1st ‘(1st ‘𝑥)) ⊆ 𝐷 ∧ ◡(1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑥))) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
92	91	simp1bi 1145	. . . . . . . . . . . . 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 4097	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍)))
96		unss12 4140	. . . . . . . . . 10 ⊢ ((((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶 ∧ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍))) → (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
97	86, 95, 96	syl2anc 584	. . . . . . . . 9 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
98		inundif 4431	. . . . . . . . . 10 ⊢ (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) = (1st ‘(1st ‘𝑥))
99	98	eqcomi 2745	. . . . . . . . 9 ⊢ (1st ‘(1st ‘𝑥)) = (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)))
100	97, 99, 1	3sstr4g 3987	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1st ‘(1st ‘𝑥)) ⊆ 𝑀)
101		ssidd 3957	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐻 ⊆ 𝐻)
102	7, 8, 45, 46, 47, 49, 100, 101	ss2mcls 35762	. . . . . . 7 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥))(mCls‘𝑇)𝐻) ⊆ (𝑀(mCls‘𝑇)𝐻))
103	89, 51	eqeltrrd 2837	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ 𝐽)
104	3, 42, 45	elmpps 35767	. . . . . . . . 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 3934	. . . . . 6 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻))
108	44, 107	rexlimddv 3143	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻))
109	3, 42, 45	elmpps 35767	. . . . 5 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ↔ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ∧ 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻)))
110	40, 108, 109	sylanbrc 583	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽)
111	1	ineq1i 4168	. . . . . . . 8 ⊢ (𝑀 ∩ (𝑍 × 𝑍)) = ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍))
112		indir 4238	. . . . . . . 8 ⊢ ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍)) = ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)))
113		disjdifr 4425	. . . . . . . . . 10 ⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) = ∅
114		0ss 4352	. . . . . . . . . 10 ⊢ ∅ ⊆ (𝐶 ∩ (𝑍 × 𝑍))
115	113, 114	eqsstri 3980	. . . . . . . . 9 ⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍))
116		ssequn2 4141	. . . . . . . . 9 ⊢ (((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍)) ↔ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍)))
117	115, 116	mpbi 230	. . . . . . . 8 ⊢ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍))
118	111, 112, 117	3eqtri 2763	. . . . . . 7 ⊢ (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍))
119	118	a1i 11	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍)))
120	119	oteq1d 4841	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩ = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
121	59, 3, 41, 63	msrval 35732	. . . . . 6 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
122	40, 121	syl 17	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
123	120, 122, 65	3eqtr4d 2781	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
124	110, 123	jca 511	. . 3 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩)))
125	124	ex 412	. 2 ⊢ (𝑇 ∈ mFS → (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 → (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))))
126	41, 42, 2	mthmi 35771	. 2 ⊢ ((⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩)) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈)
127	125, 126	impbid1 225	1 ⊢ (𝑇 ∈ mFS → (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 ↔ (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ∃wrex 3060   ∖ cdif 3898   ∪ cun 3899   ∩ cin 3900   ⊆ wss 3901  ∅c0 4285  {csn 4580  ⟨cotp 4588  ∪ cuni 4863   I cid 5518   × cxp 5622  ^◡ccnv 5623   “ cima 5627  ‘cfv 6492  (class class class)co 7358  1^st c1st 7931  2^nd c2nd 7932  Fincfn 8883  mVRcmvar 35655  mExcmex 35661  mDVcmdv 35662  mVarscmvrs 35663  mPreStcmpst 35667  mStRedcmsr 35668  mFScmfs 35670  mClscmcls 35671  mPPStcmpps 35672  mThmcmthm 35673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-ot 4589  df-uni 4864  df-int 4903  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-er 8635  df-map 8765  df-pm 8766  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-card 9851  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-nn 12146  df-2 12208  df-n0 12402  df-z 12489  df-uz 12752  df-fz 13424  df-fzo 13571  df-seq 13925  df-hash 14254  df-word 14437  df-concat 14494  df-s1 14520  df-struct 17074  df-sets 17091  df-slot 17109  df-ndx 17121  df-base 17137  df-ress 17158  df-plusg 17190  df-0g 17361  df-gsum 17362  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-submnd 18709  df-frmd 18774  df-mrex 35680  df-mex 35681  df-mdv 35682  df-mrsub 35684  df-msub 35685  df-mvh 35686  df-mpst 35687  df-msr 35688  df-msta 35689  df-mfs 35690  df-mcls 35691  df-mpps 35692  df-mthm 35693

This theorem is referenced by: (None)