mthmpps - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mthmpps		Structured version Visualization version GIF version

Theorem mthmpps 35410

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 2726	. . . . . . . . . . . . . 14 ⊢ (mPreSt‘𝑇) = (mPreSt‘𝑇)
4	2, 3	mthmsta 35406	. . . . . . . . . . . . 13 ⊢ 𝑈 ⊆ (mPreSt‘𝑇)
5		simpr 483	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈)
6	4, 5	sselid 3977	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
7		mthmpps.d	. . . . . . . . . . . . 13 ⊢ 𝐷 = (mDV‘𝑇)
8		eqid 2726	. . . . . . . . . . . . 13 ⊢ (mEx‘𝑇) = (mEx‘𝑇)
9	7, 8, 3	elmpst 35364	. . . . . . . . . . . 12 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ↔ ((𝐶 ⊆ 𝐷 ∧ ^◡𝐶 = 𝐶) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
10	6, 9	sylib 217	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ((𝐶 ⊆ 𝐷 ∧ ^◡𝐶 = 𝐶) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
11	10	simp1d 1139	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐶 ⊆ 𝐷 ∧ ^◡𝐶 = 𝐶))
12	11	simpld 493	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐶 ⊆ 𝐷)
13		difssd 4132	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐷 ∖ (𝑍 × 𝑍)) ⊆ 𝐷)
14	12, 13	unssd 4187	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ⊆ 𝐷)
15	1, 14	eqsstrid 4028	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝑀 ⊆ 𝐷)
16	11	simprd 494	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ^◡𝐶 = 𝐶)
17		cnvdif 6155	. . . . . . . . . . 11 ⊢ ^◡(𝐷 ∖ (𝑍 × 𝑍)) = (^◡𝐷 ∖ ^◡(𝑍 × 𝑍))
18		cnvdif 6155	. . . . . . . . . . . . . 14 ⊢ ^◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (^◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ^◡ I )
19		cnvxp 6168	. . . . . . . . . . . . . . 15 ⊢ ^◡((mVR‘𝑇) × (mVR‘𝑇)) = ((mVR‘𝑇) × (mVR‘𝑇))
20		cnvi 6153	. . . . . . . . . . . . . . 15 ⊢ ^◡ I = I
21	19, 20	difeq12i 4119	. . . . . . . . . . . . . 14 ⊢ (^◡((mVR‘𝑇) × (mVR‘𝑇)) ∖ ^◡ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
22	18, 21	eqtri 2754	. . . . . . . . . . . . 13 ⊢ ^◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I ) = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
23		eqid 2726	. . . . . . . . . . . . . . 15 ⊢ (mVR‘𝑇) = (mVR‘𝑇)
24	23, 7	mdvval 35332	. . . . . . . . . . . . . 14 ⊢ 𝐷 = (((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
25	24	cnveqi 5881	. . . . . . . . . . . . 13 ⊢ ^◡𝐷 = ^◡(((mVR‘𝑇) × (mVR‘𝑇)) ∖ I )
26	22, 25, 24	3eqtr4i 2764	. . . . . . . . . . . 12 ⊢ ^◡𝐷 = 𝐷
27		cnvxp 6168	. . . . . . . . . . . 12 ⊢ ^◡(𝑍 × 𝑍) = (𝑍 × 𝑍)
28	26, 27	difeq12i 4119	. . . . . . . . . . 11 ⊢ (^◡𝐷 ∖ ^◡(𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍))
29	17, 28	eqtri 2754	. . . . . . . . . 10 ⊢ ^◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍))
30	29	a1i 11	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ^◡(𝐷 ∖ (𝑍 × 𝑍)) = (𝐷 ∖ (𝑍 × 𝑍)))
31	16, 30	uneq12d 4164	. . . . . . . 8 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (^◡𝐶 ∪ ^◡(𝐷 ∖ (𝑍 × 𝑍))) = (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
32	1	cnveqi 5881	. . . . . . . . 9 ⊢ ^◡𝑀 = ^◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍)))
33		cnvun 6154	. . . . . . . . 9 ⊢ ^◡(𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) = (^◡𝐶 ∪ ^◡(𝐷 ∖ (𝑍 × 𝑍)))
34	32, 33	eqtri 2754	. . . . . . . 8 ⊢ ^◡𝑀 = (^◡𝐶 ∪ ^◡(𝐷 ∖ (𝑍 × 𝑍)))
35	31, 34, 1	3eqtr4g 2791	. . . . . . 7 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ^◡𝑀 = 𝑀)
36	15, 35	jca 510	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑀 ⊆ 𝐷 ∧ ^◡𝑀 = 𝑀))
37	10	simp2d 1140	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin))
38	10	simp3d 1141	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐴 ∈ (mEx‘𝑇))
39	7, 8, 3	elmpst 35364	. . . . . 6 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ↔ ((𝑀 ⊆ 𝐷 ∧ ^◡𝑀 = 𝑀) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
40	36, 37, 38, 39	syl3anbrc 1340	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
41		mthmpps.r	. . . . . . . 8 ⊢ 𝑅 = (mStRed‘𝑇)
42		mthmpps.j	. . . . . . . 8 ⊢ 𝐽 = (mPPSt‘𝑇)
43	41, 42, 2	elmthm 35404	. . . . . . 7 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 ↔ ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
44	5, 43	sylib 217	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ∃𝑥 ∈ 𝐽 (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
45		eqid 2726	. . . . . . . 8 ⊢ (mCls‘𝑇) = (mCls‘𝑇)
46		simpll 765	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑇 ∈ mFS)
47	15	adantr 479	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑀 ⊆ 𝐷)
48	37	simpld 493	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐻 ⊆ (mEx‘𝑇))
49	48	adantr 479	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐻 ⊆ (mEx‘𝑇))
50	3, 42	mppspst 35402	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐽 ⊆ (mPreSt‘𝑇)
51		simprl 769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 ∈ 𝐽)
52	50, 51	sselid 3977	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 ∈ (mPreSt‘𝑇))
53	3	mpst123 35368	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (mPreSt‘𝑇) → 𝑥 = ⟨(1^st ‘(1^st ‘𝑥)), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩)
54	52, 53	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 = ⟨(1^st ‘(1^st ‘𝑥)), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩)
55	54	fveq2d 6905	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘𝑥) = (𝑅‘⟨(1^st ‘(1^st ‘𝑥)), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩))
56		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
57	55, 56	eqtr3d 2768	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘⟨(1^st ‘(1^st ‘𝑥)), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
58	54, 52	eqeltrrd 2827	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1^st ‘(1^st ‘𝑥)), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩ ∈ (mPreSt‘𝑇))
59		mthmpps.v	. . . . . . . . . . . . . . . . 17 ⊢ 𝑉 = (mVars‘𝑇)
60		eqid 2726	. . . . . . . . . . . . . . . . 17 ⊢ ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) = ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)}))
61	59, 3, 41, 60	msrval 35366	. . . . . . . . . . . . . . . 16 ⊢ (⟨(1^st ‘(1^st ‘𝑥)), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩ ∈ (mPreSt‘𝑇) → (𝑅‘⟨(1^st ‘(1^st ‘𝑥)), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩) = ⟨((1^st ‘(1^st ‘𝑥)) ∩ (∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) × ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})))), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩)
62	58, 61	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘⟨(1^st ‘(1^st ‘𝑥)), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩) = ⟨((1^st ‘(1^st ‘𝑥)) ∩ (∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) × ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})))), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩)
63		mthmpps.z	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑍 = ∪ (𝑉 “ (𝐻 ∪ {𝐴}))
64	59, 3, 41, 63	msrval 35366	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝐶, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
65	6, 64	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
66	65	adantr 479	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑅‘⟨𝐶, 𝐻, 𝐴⟩) = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
67	57, 62, 66	3eqtr3d 2774	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨((1^st ‘(1^st ‘𝑥)) ∩ (∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) × ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})))), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩ = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
68		fvex 6914	. . . . . . . . . . . . . . . 16 ⊢ (1^st ‘(1^st ‘𝑥)) ∈ V
69	68	inex1 5322	. . . . . . . . . . . . . . 15 ⊢ ((1^st ‘(1^st ‘𝑥)) ∩ (∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) × ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})))) ∈ V
70		fvex 6914	. . . . . . . . . . . . . . 15 ⊢ (2^nd ‘(1^st ‘𝑥)) ∈ V
71		fvex 6914	. . . . . . . . . . . . . . 15 ⊢ (2^nd ‘𝑥) ∈ V
72	69, 70, 71	otth 5490	. . . . . . . . . . . . . 14 ⊢ (⟨((1^st ‘(1^st ‘𝑥)) ∩ (∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) × ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})))), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩ = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩ ↔ (((1^st ‘(1^st ‘𝑥)) ∩ (∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) × ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})))) = (𝐶 ∩ (𝑍 × 𝑍)) ∧ (2^nd ‘(1^st ‘𝑥)) = 𝐻 ∧ (2^nd ‘𝑥) = 𝐴))
73	67, 72	sylib 217	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (((1^st ‘(1^st ‘𝑥)) ∩ (∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) × ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})))) = (𝐶 ∩ (𝑍 × 𝑍)) ∧ (2^nd ‘(1^st ‘𝑥)) = 𝐻 ∧ (2^nd ‘𝑥) = 𝐴))
74	73	simp1d 1139	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1^st ‘(1^st ‘𝑥)) ∩ (∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) × ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})))) = (𝐶 ∩ (𝑍 × 𝑍)))
75	73	simp2d 1140	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (2^nd ‘(1^st ‘𝑥)) = 𝐻)
76	73	simp3d 1141	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (2^nd ‘𝑥) = 𝐴)
77	76	sneqd 4645	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → {(2^nd ‘𝑥)} = {𝐴})
78	75, 77	uneq12d 4164	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)}) = (𝐻 ∪ {𝐴}))
79	78	imaeq2d 6069	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) = (𝑉 “ (𝐻 ∪ {𝐴})))
80	79	unieqd 4926	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) = ∪ (𝑉 “ (𝐻 ∪ {𝐴})))
81	80, 63	eqtr4di 2784	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) = 𝑍)
82	81	sqxpeqd 5714	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) × ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)}))) = (𝑍 × 𝑍))
83	82	ineq2d 4213	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1^st ‘(1^st ‘𝑥)) ∩ (∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})) × ∪ (𝑉 “ ((2^nd ‘(1^st ‘𝑥)) ∪ {(2^nd ‘𝑥)})))) = ((1^st ‘(1^st ‘𝑥)) ∩ (𝑍 × 𝑍)))
84	74, 83	eqtr3d 2768	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (𝐶 ∩ (𝑍 × 𝑍)) = ((1^st ‘(1^st ‘𝑥)) ∩ (𝑍 × 𝑍)))
85		inss1 4230	. . . . . . . . . . 11 ⊢ (𝐶 ∩ (𝑍 × 𝑍)) ⊆ 𝐶
86	84, 85	eqsstrrdi 4035	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1^st ‘(1^st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶)
87		eqidd 2727	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1^st ‘(1^st ‘𝑥)) = (1^st ‘(1^st ‘𝑥)))
88	87, 75, 76	oteq123d 4894	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1^st ‘(1^st ‘𝑥)), (2^nd ‘(1^st ‘𝑥)), (2^nd ‘𝑥)⟩ = ⟨(1^st ‘(1^st ‘𝑥)), 𝐻, 𝐴⟩)
89	54, 88	eqtrd 2766	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝑥 = ⟨(1^st ‘(1^st ‘𝑥)), 𝐻, 𝐴⟩)
90	89, 52	eqeltrrd 2827	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1^st ‘(1^st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇))
91	7, 8, 3	elmpst 35364	. . . . . . . . . . . . . 14 ⊢ (⟨(1^st ‘(1^st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ↔ (((1^st ‘(1^st ‘𝑥)) ⊆ 𝐷 ∧ ^◡(1^st ‘(1^st ‘𝑥)) = (1^st ‘(1^st ‘𝑥))) ∧ (𝐻 ⊆ (mEx‘𝑇) ∧ 𝐻 ∈ Fin) ∧ 𝐴 ∈ (mEx‘𝑇)))
92	91	simp1bi 1142	. . . . . . . . . . . . 13 ⊢ (⟨(1^st ‘(1^st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → ((1^st ‘(1^st ‘𝑥)) ⊆ 𝐷 ∧ ^◡(1^st ‘(1^st ‘𝑥)) = (1^st ‘(1^st ‘𝑥))))
93	92	simpld 493	. . . . . . . . . . . 12 ⊢ (⟨(1^st ‘(1^st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (1^st ‘(1^st ‘𝑥)) ⊆ 𝐷)
94	90, 93	syl 17	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1^st ‘(1^st ‘𝑥)) ⊆ 𝐷)
95	94	ssdifd 4140	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1^st ‘(1^st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍)))
96		unss12 4183	. . . . . . . . . 10 ⊢ ((((1^st ‘(1^st ‘𝑥)) ∩ (𝑍 × 𝑍)) ⊆ 𝐶 ∧ ((1^st ‘(1^st ‘𝑥)) ∖ (𝑍 × 𝑍)) ⊆ (𝐷 ∖ (𝑍 × 𝑍))) → (((1^st ‘(1^st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1^st ‘(1^st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
97	86, 95, 96	syl2anc 582	. . . . . . . . 9 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (((1^st ‘(1^st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1^st ‘(1^st ‘𝑥)) ∖ (𝑍 × 𝑍))) ⊆ (𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))))
98		inundif 4483	. . . . . . . . . 10 ⊢ (((1^st ‘(1^st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1^st ‘(1^st ‘𝑥)) ∖ (𝑍 × 𝑍))) = (1^st ‘(1^st ‘𝑥))
99	98	eqcomi 2735	. . . . . . . . 9 ⊢ (1^st ‘(1^st ‘𝑥)) = (((1^st ‘(1^st ‘𝑥)) ∩ (𝑍 × 𝑍)) ∪ ((1^st ‘(1^st ‘𝑥)) ∖ (𝑍 × 𝑍)))
100	97, 99, 1	3sstr4g 4025	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → (1^st ‘(1^st ‘𝑥)) ⊆ 𝑀)
101		ssidd 4003	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐻 ⊆ 𝐻)
102	7, 8, 45, 46, 47, 49, 100, 101	ss2mcls 35396	. . . . . . 7 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ((1^st ‘(1^st ‘𝑥))(mCls‘𝑇)𝐻) ⊆ (𝑀(mCls‘𝑇)𝐻))
103	89, 51	eqeltrrd 2827	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → ⟨(1^st ‘(1^st ‘𝑥)), 𝐻, 𝐴⟩ ∈ 𝐽)
104	3, 42, 45	elmpps 35401	. . . . . . . . 9 ⊢ (⟨(1^st ‘(1^st ‘𝑥)), 𝐻, 𝐴⟩ ∈ 𝐽 ↔ (⟨(1^st ‘(1^st ‘𝑥)), 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ∧ 𝐴 ∈ ((1^st ‘(1^st ‘𝑥))(mCls‘𝑇)𝐻)))
105	104	simprbi 495	. . . . . . . 8 ⊢ (⟨(1^st ‘(1^st ‘𝑥)), 𝐻, 𝐴⟩ ∈ 𝐽 → 𝐴 ∈ ((1^st ‘(1^st ‘𝑥))(mCls‘𝑇)𝐻))
106	103, 105	syl 17	. . . . . . 7 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐴 ∈ ((1^st ‘(1^st ‘𝑥))(mCls‘𝑇)𝐻))
107	102, 106	sseldd 3980	. . . . . 6 ⊢ (((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) ∧ (𝑥 ∈ 𝐽 ∧ (𝑅‘𝑥) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻))
108	44, 107	rexlimddv 3151	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻))
109	3, 42, 45	elmpps 35401	. . . . 5 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ↔ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) ∧ 𝐴 ∈ (𝑀(mCls‘𝑇)𝐻)))
110	40, 108, 109	sylanbrc 581	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽)
111	1	ineq1i 4209	. . . . . . . 8 ⊢ (𝑀 ∩ (𝑍 × 𝑍)) = ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍))
112		indir 4277	. . . . . . . 8 ⊢ ((𝐶 ∪ (𝐷 ∖ (𝑍 × 𝑍))) ∩ (𝑍 × 𝑍)) = ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)))
113		disjdifr 4477	. . . . . . . . . 10 ⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) = ∅
114		0ss 4401	. . . . . . . . . 10 ⊢ ∅ ⊆ (𝐶 ∩ (𝑍 × 𝑍))
115	113, 114	eqsstri 4014	. . . . . . . . 9 ⊢ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍))
116		ssequn2 4184	. . . . . . . . 9 ⊢ (((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍)) ⊆ (𝐶 ∩ (𝑍 × 𝑍)) ↔ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍)))
117	115, 116	mpbi 229	. . . . . . . 8 ⊢ ((𝐶 ∩ (𝑍 × 𝑍)) ∪ ((𝐷 ∖ (𝑍 × 𝑍)) ∩ (𝑍 × 𝑍))) = (𝐶 ∩ (𝑍 × 𝑍))
118	111, 112, 117	3eqtri 2758	. . . . . . 7 ⊢ (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍))
119	118	a1i 11	. . . . . 6 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑀 ∩ (𝑍 × 𝑍)) = (𝐶 ∩ (𝑍 × 𝑍)))
120	119	oteq1d 4891	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩ = ⟨(𝐶 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
121	59, 3, 41, 63	msrval 35366	. . . . . 6 ⊢ (⟨𝑀, 𝐻, 𝐴⟩ ∈ (mPreSt‘𝑇) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
122	40, 121	syl 17	. . . . 5 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = ⟨(𝑀 ∩ (𝑍 × 𝑍)), 𝐻, 𝐴⟩)
123	120, 122, 65	3eqtr4d 2776	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))
124	110, 123	jca 510	. . 3 ⊢ ((𝑇 ∈ mFS ∧ ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈) → (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩)))
125	124	ex 411	. 2 ⊢ (𝑇 ∈ mFS → (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 → (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))))
126	41, 42, 2	mthmi 35405	. 2 ⊢ ((⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩)) → ⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈)
127	125, 126	impbid1 224	1 ⊢ (𝑇 ∈ mFS → (⟨𝐶, 𝐻, 𝐴⟩ ∈ 𝑈 ↔ (⟨𝑀, 𝐻, 𝐴⟩ ∈ 𝐽 ∧ (𝑅‘⟨𝑀, 𝐻, 𝐴⟩) = (𝑅‘⟨𝐶, 𝐻, 𝐴⟩))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1534 ∈ wcel 2099 ∃wrex 3060 ∖ cdif 3944 ∪ cun 3945 ∩ cin 3946 ⊆ wss 3947 ∅c0 4325 {csn 4633 ⟨cotp 4641 ∪ cuni 4913 I cid 5579 × cxp 5680 ^◡ccnv 5681 “ cima 5685 ‘cfv 6554 (class class class)co 7424 1^st c1st 8001 2^nd c2nd 8002 Fincfn 8974 mVRcmvar 35289 mExcmex 35295 mDVcmdv 35296 mVarscmvrs 35297 mPreStcmpst 35301 mStRedcmsr 35302 mFScmfs 35304 mClscmcls 35305 mPPStcmpps 35306 mThmcmthm 35307

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5290 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746 ax-cnex 11214 ax-resscn 11215 ax-1cn 11216 ax-icn 11217 ax-addcl 11218 ax-addrcl 11219 ax-mulcl 11220 ax-mulrcl 11221 ax-mulcom 11222 ax-addass 11223 ax-mulass 11224 ax-distr 11225 ax-i2m1 11226 ax-1ne0 11227 ax-1rid 11228 ax-rnegex 11229 ax-rrecex 11230 ax-cnre 11231 ax-pre-lttri 11232 ax-pre-lttrn 11233 ax-pre-ltadd 11234 ax-pre-mulgt0 11235

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-ot 4642 df-uni 4914 df-int 4955 df-iun 5003 df-br 5154 df-opab 5216 df-mpt 5237 df-tr 5271 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-pred 6312 df-ord 6379 df-on 6380 df-lim 6381 df-suc 6382 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-riota 7380 df-ov 7427 df-oprab 7428 df-mpo 7429 df-om 7877 df-1st 8003 df-2nd 8004 df-frecs 8296 df-wrecs 8327 df-recs 8401 df-rdg 8440 df-1o 8496 df-er 8734 df-map 8857 df-pm 8858 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-card 9982 df-pnf 11300 df-mnf 11301 df-xr 11302 df-ltxr 11303 df-le 11304 df-sub 11496 df-neg 11497 df-nn 12265 df-2 12327 df-n0 12525 df-z 12611 df-uz 12875 df-fz 13539 df-fzo 13682 df-seq 14022 df-hash 14348 df-word 14523 df-concat 14579 df-s1 14604 df-struct 17149 df-sets 17166 df-slot 17184 df-ndx 17196 df-base 17214 df-ress 17243 df-plusg 17279 df-0g 17456 df-gsum 17457 df-mgm 18633 df-sgrp 18712 df-mnd 18728 df-submnd 18774 df-frmd 18839 df-mrex 35314 df-mex 35315 df-mdv 35316 df-mrsub 35318 df-msub 35319 df-mvh 35320 df-mpst 35321 df-msr 35322 df-msta 35323 df-mfs 35324 df-mcls 35325 df-mpps 35326 df-mthm 35327

This theorem is referenced by: (None)

W3C validator