mthmpps

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)

	Ref	Expression
Hypotheses	mthmpps.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
	mthmpps.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
	mthmpps.u	⊢ 𝑈 = ( mThm ‘ 𝑇 )
	mthmpps.d	⊢ 𝐷 = ( mDV ‘ 𝑇 )
	mthmpps.v	⊢ 𝑉 = ( mVars ‘ 𝑇 )
	mthmpps.z	⊢ 𝑍 = ∪ ( 𝑉 “ ( 𝐻 ∪ { 𝐴 } ) )
	mthmpps.m	⊢ 𝑀 = ( 𝐶 ∪ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) )
Assertion	mthmpps	⊢ ( 𝑇 ∈ mFS → ( ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ↔ ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ∧ ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mthmpps.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
2		mthmpps.j	⊢ 𝐽 = ( mPPSt ‘ 𝑇 )
3		mthmpps.u	⊢ 𝑈 = ( mThm ‘ 𝑇 )
4		mthmpps.d	⊢ 𝐷 = ( mDV ‘ 𝑇 )
5		mthmpps.v	⊢ 𝑉 = ( mVars ‘ 𝑇 )
6		mthmpps.z	⊢ 𝑍 = ∪ ( 𝑉 “ ( 𝐻 ∪ { 𝐴 } ) )
7		mthmpps.m	⊢ 𝑀 = ( 𝐶 ∪ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) )
8		eqid	⊢ ( mPreSt ‘ 𝑇 ) = ( mPreSt ‘ 𝑇 )
9	3 8	mthmsta	⊢ 𝑈 ⊆ ( mPreSt ‘ 𝑇 )
10		simpr	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 )
11	9 10	sseldi	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) )
12		eqid	⊢ ( mEx ‘ 𝑇 ) = ( mEx ‘ 𝑇 )
13	4 12 8	elmpst	⊢ ( ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) ↔ ( ( 𝐶 ⊆ 𝐷 ∧ ^◡ 𝐶 = 𝐶 ) ∧ ( 𝐻 ⊆ ( mEx ‘ 𝑇 ) ∧ 𝐻 ∈ Fin ) ∧ 𝐴 ∈ ( mEx ‘ 𝑇 ) ) )
14	11 13	sylib	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( ( 𝐶 ⊆ 𝐷 ∧ ^◡ 𝐶 = 𝐶 ) ∧ ( 𝐻 ⊆ ( mEx ‘ 𝑇 ) ∧ 𝐻 ∈ Fin ) ∧ 𝐴 ∈ ( mEx ‘ 𝑇 ) ) )
15	14	simp1d	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝐶 ⊆ 𝐷 ∧ ^◡ 𝐶 = 𝐶 ) )
16	15	simpld	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → 𝐶 ⊆ 𝐷 )
17		difssd	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ⊆ 𝐷 )
18	16 17	unssd	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝐶 ∪ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) ⊆ 𝐷 )
19	7 18	eqsstrid	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → 𝑀 ⊆ 𝐷 )
20	15	simprd	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ^◡ 𝐶 = 𝐶 )
21		cnvdif	⊢ ^◡ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) = ( ^◡ 𝐷 ∖ ^◡ ( 𝑍 × 𝑍 ) )
22		cnvdif	⊢ ^◡ ( ( ( mVR ‘ 𝑇 ) × ( mVR ‘ 𝑇 ) ) ∖ I ) = ( ^◡ ( ( mVR ‘ 𝑇 ) × ( mVR ‘ 𝑇 ) ) ∖ ^◡ I )
23		cnvxp	⊢ ^◡ ( ( mVR ‘ 𝑇 ) × ( mVR ‘ 𝑇 ) ) = ( ( mVR ‘ 𝑇 ) × ( mVR ‘ 𝑇 ) )
24		cnvi	⊢ ^◡ I = I
25	23 24	difeq12i	⊢ ( ^◡ ( ( mVR ‘ 𝑇 ) × ( mVR ‘ 𝑇 ) ) ∖ ^◡ I ) = ( ( ( mVR ‘ 𝑇 ) × ( mVR ‘ 𝑇 ) ) ∖ I )
26	22 25	eqtri	⊢ ^◡ ( ( ( mVR ‘ 𝑇 ) × ( mVR ‘ 𝑇 ) ) ∖ I ) = ( ( ( mVR ‘ 𝑇 ) × ( mVR ‘ 𝑇 ) ) ∖ I )
27		eqid	⊢ ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 )
28	27 4	mdvval	⊢ 𝐷 = ( ( ( mVR ‘ 𝑇 ) × ( mVR ‘ 𝑇 ) ) ∖ I )
29	28	cnveqi	⊢ ^◡ 𝐷 = ^◡ ( ( ( mVR ‘ 𝑇 ) × ( mVR ‘ 𝑇 ) ) ∖ I )
30	26 29 28	3eqtr4i	⊢ ^◡ 𝐷 = 𝐷
31		cnvxp	⊢ ^◡ ( 𝑍 × 𝑍 ) = ( 𝑍 × 𝑍 )
32	30 31	difeq12i	⊢ ( ^◡ 𝐷 ∖ ^◡ ( 𝑍 × 𝑍 ) ) = ( 𝐷 ∖ ( 𝑍 × 𝑍 ) )
33	21 32	eqtri	⊢ ^◡ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) = ( 𝐷 ∖ ( 𝑍 × 𝑍 ) )
34	33	a1i	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ^◡ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) = ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) )
35	20 34	uneq12d	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( ^◡ 𝐶 ∪ ^◡ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) = ( 𝐶 ∪ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) )
36	7	cnveqi	⊢ ^◡ 𝑀 = ^◡ ( 𝐶 ∪ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) )
37		cnvun	⊢ ^◡ ( 𝐶 ∪ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) = ( ^◡ 𝐶 ∪ ^◡ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) )
38	36 37	eqtri	⊢ ^◡ 𝑀 = ( ^◡ 𝐶 ∪ ^◡ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) )
39	35 38 7	3eqtr4g	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ^◡ 𝑀 = 𝑀 )
40	19 39	jca	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝑀 ⊆ 𝐷 ∧ ^◡ 𝑀 = 𝑀 ) )
41	14	simp2d	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝐻 ⊆ ( mEx ‘ 𝑇 ) ∧ 𝐻 ∈ Fin ) )
42	14	simp3d	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → 𝐴 ∈ ( mEx ‘ 𝑇 ) )
43	4 12 8	elmpst	⊢ ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) ↔ ( ( 𝑀 ⊆ 𝐷 ∧ ^◡ 𝑀 = 𝑀 ) ∧ ( 𝐻 ⊆ ( mEx ‘ 𝑇 ) ∧ 𝐻 ∈ Fin ) ∧ 𝐴 ∈ ( mEx ‘ 𝑇 ) ) )
44	40 41 42 43	syl3anbrc	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) )
45	1 2 3	elmthm	⊢ ( ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) )
46	10 45	sylib	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ∃ 𝑥 ∈ 𝐽 ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) )
47		eqid	⊢ ( mCls ‘ 𝑇 ) = ( mCls ‘ 𝑇 )
48		simpll	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝑇 ∈ mFS )
49	19	adantr	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝑀 ⊆ 𝐷 )
50	41	simpld	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → 𝐻 ⊆ ( mEx ‘ 𝑇 ) )
51	50	adantr	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝐻 ⊆ ( mEx ‘ 𝑇 ) )
52	8 2	mppspst	⊢ 𝐽 ⊆ ( mPreSt ‘ 𝑇 )
53		simprl	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝑥 ∈ 𝐽 )
54	52 53	sseldi	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝑥 ∈ ( mPreSt ‘ 𝑇 ) )
55	8	mpst123	⊢ ( 𝑥 ∈ ( mPreSt ‘ 𝑇 ) → 𝑥 = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ 𝑥 ) ⟩ )
56	54 55	syl	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝑥 = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ 𝑥 ) ⟩ )
57	56	fveq2d	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ 𝑥 ) ⟩ ) )
58		simprr	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) )
59	57 58	eqtr3d	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑅 ‘ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ 𝑥 ) ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) )
60	56 54	eqeltrrd	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( mPreSt ‘ 𝑇 ) )
61		eqid	⊢ ∪ ( 𝑉 “ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∪ { ( 2^nd ‘ 𝑥 ) } ) ) = ∪ ( 𝑉 “ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∪ { ( 2^nd ‘ 𝑥 ) } ) )
62	5 8 1 61	msrval	⊢ ( ⟨ ( 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 ‘ 𝑥 ) ⟩ )
63	60 62	syl	⊢ ( ( ( 𝑇 ∈ 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 ‘ 𝑥 ) ⟩ )
64	5 8 1 6	msrval	⊢ ( ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
65	11 64	syl	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
66	65	adantr	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
67	59 63 66	3eqtr3d	⊢ ( ( ( 𝑇 ∈ 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	⊢ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∈ V
69	68	inex1	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∩ ( ∪ ( 𝑉 “ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∪ { ( 2^nd ‘ 𝑥 ) } ) ) × ∪ ( 𝑉 “ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∪ { ( 2^nd ‘ 𝑥 ) } ) ) ) ) ∈ V
70		fvex	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∈ V
71		fvex	⊢ ( 2^nd ‘ 𝑥 ) ∈ V
72	69 70 71	otth	⊢ ( ⟨ ( ( 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	⊢ ( ( ( 𝑇 ∈ 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	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∩ ( ∪ ( 𝑉 “ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∪ { ( 2^nd ‘ 𝑥 ) } ) ) × ∪ ( 𝑉 “ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∪ { ( 2^nd ‘ 𝑥 ) } ) ) ) ) = ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) )
75	73	simp2d	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = 𝐻 )
76	73	simp3d	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 2^nd ‘ 𝑥 ) = 𝐴 )
77	76	sneqd	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → { ( 2^nd ‘ 𝑥 ) } = { 𝐴 } )
78	75 77	uneq12d	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∪ { ( 2^nd ‘ 𝑥 ) } ) = ( 𝐻 ∪ { 𝐴 } ) )
79	78	imaeq2d	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑉 “ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∪ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝑉 “ ( 𝐻 ∪ { 𝐴 } ) ) )
80	79	unieqd	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ∪ ( 𝑉 “ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∪ { ( 2^nd ‘ 𝑥 ) } ) ) = ∪ ( 𝑉 “ ( 𝐻 ∪ { 𝐴 } ) ) )
81	80 6	eqtr4di	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ∪ ( 𝑉 “ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∪ { ( 2^nd ‘ 𝑥 ) } ) ) = 𝑍 )
82	81	sqxpeqd	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ∪ ( 𝑉 “ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∪ { ( 2^nd ‘ 𝑥 ) } ) ) × ∪ ( 𝑉 “ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∪ { ( 2^nd ‘ 𝑥 ) } ) ) ) = ( 𝑍 × 𝑍 ) )
83	82	ineq2d	⊢ ( ( ( 𝑇 ∈ 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	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) )
85		inss1	⊢ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) ⊆ 𝐶
86	84 85	eqsstrrdi	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) ⊆ 𝐶 )
87		eqidd	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) )
88	87 75 76	oteq123d	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ 𝑥 ) ⟩ = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , 𝐻 , 𝐴 ⟩ )
89	56 88	eqtrd	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝑥 = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , 𝐻 , 𝐴 ⟩ )
90	89 54	eqeltrrd	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) )
91	4 12 8	elmpst	⊢ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) ↔ ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ⊆ 𝐷 ∧ ^◡ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ) ∧ ( 𝐻 ⊆ ( mEx ‘ 𝑇 ) ∧ 𝐻 ∈ Fin ) ∧ 𝐴 ∈ ( mEx ‘ 𝑇 ) ) )
92	91	simp1bi	⊢ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) → ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ⊆ 𝐷 ∧ ^◡ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ) )
93	92	simpld	⊢ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) → ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ⊆ 𝐷 )
94	90 93	syl	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ⊆ 𝐷 )
95	94	ssdifd	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∖ ( 𝑍 × 𝑍 ) ) ⊆ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) )
96		unss12	⊢ ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) ⊆ 𝐶 ∧ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∖ ( 𝑍 × 𝑍 ) ) ⊆ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∖ ( 𝑍 × 𝑍 ) ) ) ⊆ ( 𝐶 ∪ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) )
97	86 95 96	syl2anc	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∖ ( 𝑍 × 𝑍 ) ) ) ⊆ ( 𝐶 ∪ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) )
98		inundif	⊢ ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∖ ( 𝑍 × 𝑍 ) ) ) = ( 1^st ‘ ( 1^st ‘ 𝑥 ) )
99	98	eqcomi	⊢ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∖ ( 𝑍 × 𝑍 ) ) )
100	97 99 7	3sstr4g	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ⊆ 𝑀 )
101		ssidd	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝐻 ⊆ 𝐻 )
102	4 12 47 48 49 51 100 101	ss2mcls	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( mCls ‘ 𝑇 ) 𝐻 ) ⊆ ( 𝑀 ( mCls ‘ 𝑇 ) 𝐻 ) )
103	89 53	eqeltrrd	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ 𝐽 )
104	8 2 47	elmpps	⊢ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ↔ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) ∧ 𝐴 ∈ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( mCls ‘ 𝑇 ) 𝐻 ) ) )
105	104	simprbi	⊢ ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ 𝐽 → 𝐴 ∈ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( mCls ‘ 𝑇 ) 𝐻 ) )
106	103 105	syl	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝐴 ∈ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( mCls ‘ 𝑇 ) 𝐻 ) )
107	102 106	sseldd	⊢ ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝑅 ‘ 𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝐴 ∈ ( 𝑀 ( mCls ‘ 𝑇 ) 𝐻 ) )
108	46 107	rexlimddv	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → 𝐴 ∈ ( 𝑀 ( mCls ‘ 𝑇 ) 𝐻 ) )
109	8 2 47	elmpps	⊢ ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ↔ ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) ∧ 𝐴 ∈ ( 𝑀 ( mCls ‘ 𝑇 ) 𝐻 ) ) )
110	44 108 109	sylanbrc	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 )
111	7	ineq1i	⊢ ( 𝑀 ∩ ( 𝑍 × 𝑍 ) ) = ( ( 𝐶 ∪ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) ∩ ( 𝑍 × 𝑍 ) )
112		indir	⊢ ( ( 𝐶 ∪ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) ∩ ( 𝑍 × 𝑍 ) ) = ( ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ∩ ( 𝑍 × 𝑍 ) ) )
113		incom	⊢ ( ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ∩ ( 𝑍 × 𝑍 ) ) = ( ( 𝑍 × 𝑍 ) ∩ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) )
114		disjdif	⊢ ( ( 𝑍 × 𝑍 ) ∩ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) = ∅
115	113 114	eqtri	⊢ ( ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ∩ ( 𝑍 × 𝑍 ) ) = ∅
116		0ss	⊢ ∅ ⊆ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) )
117	115 116	eqsstri	⊢ ( ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ∩ ( 𝑍 × 𝑍 ) ) ⊆ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) )
118		ssequn2	⊢ ( ( ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ∩ ( 𝑍 × 𝑍 ) ) ⊆ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) ↔ ( ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ∩ ( 𝑍 × 𝑍 ) ) ) = ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) )
119	117 118	mpbi	⊢ ( ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ∩ ( 𝑍 × 𝑍 ) ) ) = ( 𝐶 ∩ ( 𝑍 × 𝑍 ) )
120	111 112 119	3eqtri	⊢ ( 𝑀 ∩ ( 𝑍 × 𝑍 ) ) = ( 𝐶 ∩ ( 𝑍 × 𝑍 ) )
121	120	a1i	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝑀 ∩ ( 𝑍 × 𝑍 ) ) = ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) )
122	121	oteq1d	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ⟨ ( 𝑀 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ = ⟨ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
123	5 8 1 6	msrval	⊢ ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝑀 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
124	44 123	syl	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝑀 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
125	122 124 65	3eqtr4d	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) )
126	110 125	jca	⊢ ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ∧ ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) )
127	126	ex	⊢ ( 𝑇 ∈ mFS → ( ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 → ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ∧ ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) )
128	1 2 3	mthmi	⊢ ( ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ∧ ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) → ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 )
129	127 128	impbid1	⊢ ( 𝑇 ∈ mFS → ( ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ↔ ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ∧ ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) )

Metamath Proof Explorer

Theorem mthmpps

Proof