Theorem mthmpps 35647

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 2733	. . . . . . . . . . . . . 14 ⊢ (mPreSt‘𝑇) = (mPreSt‘𝑇)
4	2, 3	mthmsta 35643	. . . . . . . . . . . . 13 ⊢ 𝑈 ⊆ (mPreSt‘𝑇)
5		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈)
6	4, 5	sselid 3928	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
7		mthmpps.d	. . . . . . . . . . . . 13 ⊢ 𝐷 = (mDV‘𝑇)
8		eqid 2733	. . . . . . . . . . . . 13 ⊢ (mEx‘𝑇) = (mEx‘𝑇)
9	7, 8, 3	elmpst 35601	. . . . . . . . . . . 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 4086	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐷 ∖ (𝑍 × 𝑍)) ⊆ 𝐷)
14	12, 13	unssd 4141	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ⊆ 𝐷)
15	1, 14	eqsstrid 3969	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝑀 ⊆ 𝐷)
16	11	simprd 495	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ◡𝐶 = 𝐶)
17		cnvdif 6095	. . . . . . . . . . 11 ⊢ ◡(𝐷 ∖ (𝑍 × 𝑍)) = (◡𝐷 ∖ ◡(𝑍 × 𝑍))
18		cnvdif 6095	. . . . . . . . . . . . . 14 ⊢ ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ◡ I )
19		cnvxp 6109	. . . . . . . . . . . . . . 15 ⊢ ◡((mVR‘𝑇) × (mVR‘𝑇)) = ((mVR‘𝑇) × (mVR‘𝑇))
20		cnvi 6093	. . . . . . . . . . . . . . 15 ⊢ ◡ I = I
21	19, 20	difeq12i 4073	. . . . . . . . . . . . . 14 ⊢ (◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ◡ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
22	18, 21	eqtri 2756	. . . . . . . . . . . . 13 ⊢ ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
23		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ (mVR‘𝑇) = (mVR‘𝑇)
24	23, 7	mdvval 35569	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
25	24	cnveqi 5818	. . . . . . . . . . . . 13 ⊢ ◡𝐷 = ◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
26	22, 25, 24	3eqtr4i 2766	. . . . . . . . . . . 12 ⊢ ◡𝐷 = 𝐷
27		cnvxp 6109	. . . . . . . . . . . 12 ⊢ ◡(𝑍 × 𝑍) = (𝑍 × 𝑍)
28	26, 27	difeq12i 4073	. . . . . . . . . . 11 ⊢ (◡𝐷 ∖ ◡(𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍))
29	17, 28	eqtri 2756	. . . . . . . . . 10 ⊢ ◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍))
30	29	a1i 11	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍)))
31	16, 30	uneq12d 4118	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍))) = (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
32	1	cnveqi 5818	. . . . . . . . 9 ⊢ ◡𝑀 = ◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))
33		cnvun 6094	. . . . . . . . 9 ⊢ ◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) = (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍)))
34	32, 33	eqtri 2756	. . . . . . . 8 ⊢ ◡𝑀 = (◡𝐶 ∪ ◡(𝐷 ∖ (𝑍 × 𝑍)))
35	31, 34, 1	3eqtr4g 2793	. . . . . . 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 35601	. . . . . 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 35641	. . . . . . 7 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 ↔ ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
44	5, 43	sylib 218	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
45		eqid 2733	. . . . . . . 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 35639	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐽 ⊆ (mPreSt‘𝑇)
51		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 ∈ 𝐽)
52	50, 51	sselid 3928	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 ∈ (mPreSt‘𝑇))
53	3	mpst123 35605	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (mPreSt‘𝑇) → 𝑥 = ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩)
54	52, 53	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 = ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩)
55	54	fveq2d 6832	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘𝑥) = (𝑅‘⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩))
56		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
57	55, 56	eqtr3d 2770	. . . . . . . . . . . . . . 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 2733	. . . . . . . . . . . . . . . . 17 ⊢ ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}))
61	59, 3, 41, 60	msrval 35603	. . . . . . . . . . . . . . . 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 35603	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
65	6, 64	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
66	65	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
67	57, 62, 66	3eqtr3d 2776	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩ = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
68		fvex 6841	. . . . . . . . . . . . . . . 16 ⊢ (1st ‘(1st ‘𝑥)) ∈ V
69	68	inex1 5257	. . . . . . . . . . . . . . 15 ⊢ ((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) ∈ V
70		fvex 6841	. . . . . . . . . . . . . . 15 ⊢ (2nd ‘(1st ‘𝑥)) ∈ V
71		fvex 6841	. . . . . . . . . . . . . . 15 ⊢ (2nd ‘𝑥) ∈ V
72	69, 70, 71	otth 5427	. . . . . . . . . . . . . 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 4587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → {(2nd ‘𝑥)} = {𝐴})
78	75, 77	uneq12d 4118	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}) = (𝐻 ∪ {𝐴}))
79	78	imaeq2d 6013	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = (𝑉 “ (𝐻 ∪ {𝐴})))
80	79	unieqd 4871	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = ∪ (𝑉 “ (𝐻 ∪ {𝐴})))
81	80, 63	eqtr4di 2786	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) = 𝑍)
82	81	sqxpeqd 5651	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)}))) = (𝑍 × 𝑍))
83	82	ineq2d 4169	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∩ (∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})) × ∪ (𝑉 “ ((2nd ‘(1st ‘𝑥)) ∪ {(2nd ‘𝑥)})))) = ((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)))
84	74, 83	eqtr3d 2770	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝐶 ∩ (𝑍 × 𝑍)) = ((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)))
85		inss1 4186	. . . . . . . . . . 11 ⊢ (𝐶 ∩ (𝑍 × 𝑍)) ⊆ 𝐶
86	84, 85	eqsstrrdi 3976	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶)
87		eqidd 2734	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑥)))
88	87, 75, 76	oteq123d 4839	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), (2nd ‘(1st ‘𝑥)), (2nd ‘𝑥)⟩ = ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩)
89	54, 88	eqtrd 2768	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 = ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩)
90	89, 52	eqeltrrd 2834	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
91	7, 8, 3	elmpst 35601	. . . . . . . . . . . . . 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 4094	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍)))
96		unss12 4137	. . . . . . . . . 10 ⊢ ((((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶 ∧ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍))) → (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
97	86, 95, 96	syl2anc 584	. . . . . . . . 9 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
98		inundif 4428	. . . . . . . . . 10 ⊢ (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍))) = (1st ‘(1st ‘𝑥))
99	98	eqcomi 2742	. . . . . . . . 9 ⊢ (1st ‘(1st ‘𝑥)) = (((1st ‘(1st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1st ‘(1st ‘𝑥)) ∖ (𝑍 × 𝑍)))
100	97, 99, 1	3sstr4g 3984	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1st ‘(1st ‘𝑥)) ⊆ 𝑀)
101		ssidd 3954	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐻 ⊆ 𝐻)
102	7, 8, 45, 46, 47, 49, 100, 101	ss2mcls 35633	. . . . . . 7 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1st ‘(1st ‘𝑥))(mCls‘𝑇)𝐻) ⊆ (𝑀(mCls‘𝑇)𝐻))
103	89, 51	eqeltrrd 2834	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1st ‘(1st ‘𝑥)), 𝐻, 𝐴⟩ ∈ 𝐽)
104	3, 42, 45	elmpps 35638	. . . . . . . . 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 3931	. . . . . 6 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻))
108	44, 107	rexlimddv 3140	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻))
109	3, 42, 45	elmpps 35638	. . . . 5 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ↔ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ∧ 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻)))
110	40, 108, 109	sylanbrc 583	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽)
111	1	ineq1i 4165	. . . . . . . 8 ⊢ (𝑀 ∩ (𝑍 × 𝑍)) = ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍))
112		indir 4235	. . . . . . . 8 ⊢ ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍)) = ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)))
113		disjdifr 4422	. . . . . . . . . 10 ⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) = ∅
114		0ss 4349	. . . . . . . . . 10 ⊢ ∅ ⊆ (𝐶 ∩ (𝑍 × 𝑍))
115	113, 114	eqsstri 3977	. . . . . . . . 9 ⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍))
116		ssequn2 4138	. . . . . . . . 9 ⊢ (((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍)) ↔ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍)))
117	115, 116	mpbi 230	. . . . . . . 8 ⊢ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍))
118	111, 112, 117	3eqtri 2760	. . . . . . 7 ⊢ (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍))
119	118	a1i 11	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍)))
120	119	oteq1d 4836	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩ = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
121	59, 3, 41, 63	msrval 35603	. . . . . 6 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
122	40, 121	syl 17	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
123	120, 122, 65	3eqtr4d 2778	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
124	110, 123	jca 511	. . 3 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩)))
125	124	ex 412	. 2 ⊢ (𝑇 ∈ mFS → (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 → (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))))
126	41, 42, 2	mthmi 35642	. 2 ⊢ ((⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩)) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈)
127	125, 126	impbid1 225	1 ⊢ (𝑇 ∈ mFS → (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 ↔ (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ∃wrex 3057   ∖ cdif 3895   ∪ cun 3896   ∩ cin 3897   ⊆ wss 3898  ∅c0 4282  {csn 4575  ⟨cotp 4583  ∪ cuni 4858   I cid 5513   × cxp 5617  ^◡ccnv 5618   “ cima 5622  ‘cfv 6486  (class class class)co 7352  1^st c1st 7925  2^nd c2nd 7926  Fincfn 8875  mVRcmvar 35526  mExcmex 35532  mDVcmdv 35533  mVarscmvrs 35534  mPreStcmpst 35538  mStRedcmsr 35539  mFScmfs 35541  mClscmcls 35542  mPPStcmpps 35543  mThmcmthm 35544

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 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11069  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089  ax-pre-mulgt0 11090

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-ot 4584  df-uni 4859  df-int 4898  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-om 7803  df-1st 7927  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-1o 8391  df-er 8628  df-map 8758  df-pm 8759  df-en 8876  df-dom 8877  df-sdom 8878  df-fin 8879  df-card 9839  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-sub 11353  df-neg 11354  df-nn 12133  df-2 12195  df-n0 12389  df-z 12476  df-uz 12739  df-fz 13410  df-fzo 13557  df-seq 13911  df-hash 14240  df-word 14423  df-concat 14480  df-s1 14506  df-struct 17060  df-sets 17077  df-slot 17095  df-ndx 17107  df-base 17123  df-ress 17144  df-plusg 17176  df-0g 17347  df-gsum 17348  df-mgm 18550  df-sgrp 18629  df-mnd 18645  df-submnd 18694  df-frmd 18759  df-mrex 35551  df-mex 35552  df-mdv 35553  df-mrsub 35555  df-msub 35556  df-mvh 35557  df-mpst 35558  df-msr 35559  df-msta 35560  df-mfs 35561  df-mcls 35562  df-mpps 35563  df-mthm 35564

This theorem is referenced by: (None)