Theorem mthmpps 35817

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 2740	. . . . . . . . . . . . . 14 ⊢ (mPreSt‘𝑇) = (mPreSt‘𝑇)
4	2, 3	mthmsta 35813	. . . . . . . . . . . . 13 ⊢ 𝑈 ⊆ (mPreSt‘𝑇)
5		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈)
6	4, 5	sselid 3920	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
7		mthmpps.d	. . . . . . . . . . . . 13 ⊢ 𝐷 = (mDV‘𝑇)
8		eqid 2740	. . . . . . . . . . . . 13 ⊢ (mEx‘𝑇) = (mEx‘𝑇)
9	7, 8, 3	elmpst 35771	. . . . . . . . . . . 12 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ↔ ((𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
10	6, 9	sylib 219	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ((𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
11	10	simp1d 1148	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐶 ⊆ 𝐷 ∧ ◡𝐶 = 𝐶))
12	11	simpld 495	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐶 ⊆ 𝐷)
13		difssd 4074	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐷 ∖ (𝑍 × 𝑍)) ⊆ 𝐷)
14	12, 13	unssd 4128	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ⊆ 𝐷)
15	1, 14	eqsstrid 3960	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝑀 ⊆ 𝐷)
16	11	simprd 496	. . . . . . . . 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 4062	. . . . . . . . . . . . . 14 ⊢ (◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ◡ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
22	18, 21	eqtri 2763	. . . . . . . . . . . . 13 ⊢ ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
23		eqid 2740	. . . . . . . . . . . . . . 15 ⊢ (mVR‘𝑇) = (mVR‘𝑇)
24	23, 7	mdvval 35739	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
25	24	cnveqi 5823	. . . . . . . . . . . . 13 ⊢ ◡𝐷 = ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
26	22, 25, 24	3eqtr4i 2773	. . . . . . . . . . . 12 ⊢ ◡𝐷 = 𝐷
27		cnvxp 6115	. . . . . . . . . . . 12 ⊢ ◡(𝑍 × 𝑍) = (𝑍 × 𝑍)
28	26, 27	difeq12i 4062	. . . . . . . . . . 11 ⊢ (◡𝐷 ∖ ◡(𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍))
29	17, 28	eqtri 2763	. . . . . . . . . 10 ⊢ ◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍))
30	29	a1i 11	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍)))
31	16, 30	uneq12d 4106	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍))) = (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
32	1	cnveqi 5823	. . . . . . . . 9 ⊢ ◡𝑀 = ◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))
33		cnvun 6100	. . . . . . . . 9 ⊢ ◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) = (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍)))
34	32, 33	eqtri 2763	. . . . . . . 8 ⊢ ◡𝑀 = (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍)))
35	31, 34, 1	3eqtr4g 2800	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ◡𝑀 = 𝑀)
36	15, 35	jca 516	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀))
37	10	simp2d 1149	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin))
38	10	simp3d 1150	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐴 ∈ (mEx‘𝑇))
39	7, 8, 3	elmpst 35771	. . . . . 6 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ↔ ((𝑀 ⊆ 𝐷 ∧ ◡𝑀 = 𝑀) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
40	36, 37, 38, 39	syl3anbrc 1350	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
41		mthmpps.r	. . . . . . . 8 ⊢ 𝑅 = (mStRed‘𝑇)
42		mthmpps.j	. . . . . . . 8 ⊢ 𝐽 = (mPPSt‘𝑇)
43	41, 42, 2	elmthm 35811	. . . . . . 7 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 ↔ ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
44	5, 43	sylib 219	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
45		eqid 2740	. . . . . . . 8 ⊢ (mCls‘𝑇) = (mCls‘𝑇)
46		simpll 772	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑇 ∈ mFS)
47	15	adantr 481	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑀 ⊆ 𝐷)
48	37	simpld 495	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐻 ⊆ (mEx‘𝑇))
49	48	adantr 481	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐻 ⊆ (mEx‘𝑇))
50	3, 42	mppspst 35809	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐽 ⊆ (mPreSt‘𝑇)
51		simprl 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 ∈ 𝐽)
52	50, 51	sselid 3920	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 ∈ (mPreSt‘𝑇))
53	3	mpst123 35775	. . . . . . . . . . . . . . . . . 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 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
57	55, 56	eqtr3d 2777	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
58	54, 52	eqeltrrd 2841	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩ ∈ (mPreSt‘𝑇))
59		mthmpps.v	. . . . . . . . . . . . . . . . 17 ⊢ 𝑉 = (mVars‘𝑇)
60		eqid 2740	. . . . . . . . . . . . . . . . 17 ⊢ ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}))
61	59, 3, 41, 60	msrval 35773	. . . . . . . . . . . . . . . 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 35773	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
65	6, 64	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
66	65	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
67	57, 62, 66	3eqtr3d 2783	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩ = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
68		fvex 6847	. . . . . . . . . . . . . . . 16 ⊢ (1st ‘(1st ‘𝑥)) ∈ V
69	68	inex1 5252	. . . . . . . . . . . . . . 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 5431	. . . . . . . . . . . . . 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 219	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = (𝐶 ∩ (𝑍 × 𝑍)) ∧ (2nd ‘(1st ‘𝑥)) = 𝐻 ∧ (2nd ‘𝑥) = 𝐴))
74	73	simp1d 1148	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = (𝐶 ∩ (𝑍 × 𝑍)))
75	73	simp2d 1149	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (2nd ‘(1st ‘𝑥)) = 𝐻)
76	73	simp3d 1150	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (2nd ‘𝑥) = 𝐴)
77	76	sneqd 4574	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → {(2nd ‘𝑥)} = {𝐴})
78	75, 77	uneq12d 4106	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}) = (𝐻 ∪ {𝐴}))
79	78	imaeq2d 6019	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = (𝑉 “ (𝐻 ∪ {𝐴})))
80	79	unieqd 4858	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = ∪ (𝑉 “ (𝐻 ∪ {𝐴})))
81	80, 63	eqtr4di 2793	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = 𝑍)
82	81	sqxpeqd 5657	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}))) = (𝑍 × 𝑍))
83	82	ineq2d 4156	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = ((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)))
84	74, 83	eqtr3d 2777	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝐶 ∩ (𝑍 × 𝑍)) = ((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)))
85		inss1 4172	. . . . . . . . . . 11 ⊢ (𝐶 ∩ (𝑍 × 𝑍)) ⊆ 𝐶
86	84, 85	eqsstrrdi 3967	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶)
87		eqidd 2741	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑥)))
88	87, 75, 76	oteq123d 4826	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩ = ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩)
89	54, 88	eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 = ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩)
90	89, 52	eqeltrrd 2841	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
91	7, 8, 3	elmpst 35771	. . . . . . . . . . . . . 14 ⊢ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ↔ (((1st ‘(1st ‘𝑥)) ⊆ 𝐷 ∧ ◡(1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑥))) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
92	91	simp1bi 1151	. . . . . . . . . . . . 13 ⊢ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → ((1st ‘(1st ‘𝑥)) ⊆ 𝐷 ∧ ◡(1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑥))))
93	92	simpld 495	. . . . . . . . . . . 12 ⊢ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (1st ‘(1st ‘𝑥)) ⊆ 𝐷)
94	90, 93	syl 17	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1st ‘(1st ‘𝑥)) ⊆ 𝐷)
95	94	ssdifd 4082	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍)))
96		unss12 4124	. . . . . . . . . 10 ⊢ ((((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶 ∧ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍))) → (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
97	86, 95, 96	syl2anc 590	. . . . . . . . 9 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
98		inundif 4414	. . . . . . . . . 10 ⊢ (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) = (1st ‘(1st ‘𝑥))
99	98	eqcomi 2749	. . . . . . . . 9 ⊢ (1st ‘(1st ‘𝑥)) = (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)))
100	97, 99, 1	3sstr4g 3975	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1st ‘(1st ‘𝑥)) ⊆ 𝑀)
101		ssidd 3945	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐻 ⊆ 𝐻)
102	7, 8, 45, 46, 47, 49, 100, 101	ss2mcls 35803	. . . . . . 7 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥))(mCls‘𝑇)𝐻) ⊆ (𝑀(mCls‘𝑇)𝐻))
103	89, 51	eqeltrrd 2841	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ 𝐽)
104	3, 42, 45	elmpps 35808	. . . . . . . . 9 ⊢ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ 𝐽 ↔ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ∧ 𝐴 ∈ ((1st ‘(1st ‘𝑥))(mCls‘𝑇)𝐻)))
105	104	simprbi 498	. . . . . . . 8 ⊢ (⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ 𝐽 → 𝐴 ∈ ((1st ‘(1st ‘𝑥))(mCls‘𝑇)𝐻))
106	103, 105	syl 17	. . . . . . 7 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐴 ∈ ((1st ‘(1st ‘𝑥))(mCls‘𝑇)𝐻))
107	102, 106	sseldd 3923	. . . . . 6 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻))
108	44, 107	rexlimddv 3147	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻))
109	3, 42, 45	elmpps 35808	. . . . 5 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ↔ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ∧ 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻)))
110	40, 108, 109	sylanbrc 589	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽)
111	1	ineq1i 4152	. . . . . . . 8 ⊢ (𝑀 ∩ (𝑍 × 𝑍)) = ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍))
112		indir 4221	. . . . . . . 8 ⊢ ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍)) = ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)))
113		disjdifr 4408	. . . . . . . . . 10 ⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) = ∅
114		0ss 4335	. . . . . . . . . 10 ⊢ ∅ ⊆ (𝐶 ∩ (𝑍 × 𝑍))
115	113, 114	eqsstri 3968	. . . . . . . . 9 ⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍))
116		ssequn2 4125	. . . . . . . . 9 ⊢ (((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍)) ↔ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍)))
117	115, 116	mpbi 231	. . . . . . . 8 ⊢ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍))
118	111, 112, 117	3eqtri 2767	. . . . . . 7 ⊢ (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍))
119	118	a1i 11	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍)))
120	119	oteq1d 4823	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩ = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
121	59, 3, 41, 63	msrval 35773	. . . . . 6 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
122	40, 121	syl 17	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
123	120, 122, 65	3eqtr4d 2785	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
124	110, 123	jca 516	. . 3 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩)))
125	124	ex 413	. 2 ⊢ (𝑇 ∈ mFS → (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 → (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))))
126	41, 42, 2	mthmi 35812	. 2 ⊢ ((⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩)) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈)
127	125, 126	impbid1 226	1 ⊢ (𝑇 ∈ mFS → (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 ↔ (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∃wrex 3064   ∖ cdif 3887   ∪ cun 3888   ∩ cin 3889   ⊆ wss 3890  ∅c0 4268  {csn 4562  ⟨cotp 4570  ∪ cuni 4845   I cid 5519   × cxp 5623  ^◡ccnv 5624   “ cima 5628  ‘cfv 6492  (class class class)co 7363  1^st c1st 7936  2^nd c2nd 7937  Fincfn 8890  mVRcmvar 35696  mExcmex 35702  mDVcmdv 35703  mVarscmvrs 35704  mPreStcmpst 35708  mStRedcmsr 35709  mFScmfs 35711  mClscmcls 35712  mPPStcmpps 35713  mThmcmthm 35714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-ot 4571  df-uni 4846  df-int 4885  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-om 7814  df-1st 7938  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-er 8640  df-map 8772  df-pm 8773  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-card 9861  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-nn 12173  df-2 12242  df-n0 12436  df-z 12523  df-uz 12787  df-fz 13460  df-fzo 13607  df-seq 13962  df-hash 14291  df-word 14474  df-concat 14531  df-s1 14557  df-struct 17115  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17178  df-ress 17199  df-plusg 17231  df-0g 17402  df-gsum 17403  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-submnd 18750  df-frmd 18815  df-mrex 35721  df-mex 35722  df-mdv 35723  df-mrsub 35725  df-msub 35726  df-mvh 35727  df-mpst 35728  df-msr 35729  df-msta 35730  df-mfs 35731  df-mcls 35732  df-mpps 35733  df-mthm 35734

This theorem is referenced by: (None)