Metamath Proof Explorer


Theorem 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 ‘ 𝑇 ) → 𝑥 = ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd𝑥 ) ⟩ )
56 54 55 syl ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝑥 = ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd𝑥 ) ⟩ )
57 56 fveq2d ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd𝑥 ) ⟩ ) )
58 simprr ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) )
59 57 58 eqtr3d ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑅 ‘ ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd𝑥 ) ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) )
60 56 54 eqeltrrd ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd𝑥 ) ⟩ ∈ ( mPreSt ‘ 𝑇 ) )
61 eqid ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) = ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) )
62 5 8 1 61 msrval ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd𝑥 ) ⟩ ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd𝑥 ) ⟩ ) = ⟨ ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) × ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) ) ) , ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd𝑥 ) ⟩ )
63 60 62 syl ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑅 ‘ ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd𝑥 ) ⟩ ) = ⟨ ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) × ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) ) ) , ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd𝑥 ) ⟩ )
64 5 8 1 6 msrval ( ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
65 11 64 syl ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
66 65 adantr ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
67 59 63 66 3eqtr3d ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ⟨ ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) × ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) ) ) , ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd𝑥 ) ⟩ = ⟨ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
68 fvex ( 1st ‘ ( 1st𝑥 ) ) ∈ V
69 68 inex1 ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) × ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) ) ) ∈ V
70 fvex ( 2nd ‘ ( 1st𝑥 ) ) ∈ V
71 fvex ( 2nd𝑥 ) ∈ V
72 69 70 71 otth ( ⟨ ( ( 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 ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) × ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) ) ) = ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) ∧ ( 2nd ‘ ( 1st𝑥 ) ) = 𝐻 ∧ ( 2nd𝑥 ) = 𝐴 ) )
74 73 simp1d ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) × ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) ) ) = ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) )
75 73 simp2d ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 2nd ‘ ( 1st𝑥 ) ) = 𝐻 )
76 73 simp3d ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 2nd𝑥 ) = 𝐴 )
77 76 sneqd ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → { ( 2nd𝑥 ) } = { 𝐴 } )
78 75 77 uneq12d ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) = ( 𝐻 ∪ { 𝐴 } ) )
79 78 imaeq2d ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) = ( 𝑉 “ ( 𝐻 ∪ { 𝐴 } ) ) )
80 79 unieqd ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) = ( 𝑉 “ ( 𝐻 ∪ { 𝐴 } ) ) )
81 80 6 eqtr4di ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) = 𝑍 )
82 81 sqxpeqd ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) × ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) ) = ( 𝑍 × 𝑍 ) )
83 82 ineq2d ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) × ( 𝑉 “ ( ( 2nd ‘ ( 1st𝑥 ) ) ∪ { ( 2nd𝑥 ) } ) ) ) ) = ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) )
84 74 83 eqtr3d ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) = ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) )
85 inss1 ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) ⊆ 𝐶
86 84 85 eqsstrrdi ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) ⊆ 𝐶 )
87 eqidd ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 1st ‘ ( 1st𝑥 ) ) = ( 1st ‘ ( 1st𝑥 ) ) )
88 87 75 76 oteq123d ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ⟨ ( 1st ‘ ( 1st𝑥 ) ) , ( 2nd ‘ ( 1st𝑥 ) ) , ( 2nd𝑥 ) ⟩ = ⟨ ( 1st ‘ ( 1st𝑥 ) ) , 𝐻 , 𝐴 ⟩ )
89 56 88 eqtrd ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝑥 = ⟨ ( 1st ‘ ( 1st𝑥 ) ) , 𝐻 , 𝐴 ⟩ )
90 89 54 eqeltrrd ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ⟨ ( 1st ‘ ( 1st𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) )
91 4 12 8 elmpst ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) ↔ ( ( ( 1st ‘ ( 1st𝑥 ) ) ⊆ 𝐷 ( 1st ‘ ( 1st𝑥 ) ) = ( 1st ‘ ( 1st𝑥 ) ) ) ∧ ( 𝐻 ⊆ ( mEx ‘ 𝑇 ) ∧ 𝐻 ∈ Fin ) ∧ 𝐴 ∈ ( mEx ‘ 𝑇 ) ) )
92 91 simp1bi ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) → ( ( 1st ‘ ( 1st𝑥 ) ) ⊆ 𝐷 ( 1st ‘ ( 1st𝑥 ) ) = ( 1st ‘ ( 1st𝑥 ) ) ) )
93 92 simpld ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) → ( 1st ‘ ( 1st𝑥 ) ) ⊆ 𝐷 )
94 90 93 syl ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 1st ‘ ( 1st𝑥 ) ) ⊆ 𝐷 )
95 94 ssdifd ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( 1st ‘ ( 1st𝑥 ) ) ∖ ( 𝑍 × 𝑍 ) ) ⊆ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) )
96 unss12 ( ( ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) ⊆ 𝐶 ∧ ( ( 1st ‘ ( 1st𝑥 ) ) ∖ ( 𝑍 × 𝑍 ) ) ⊆ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) → ( ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 1st ‘ ( 1st𝑥 ) ) ∖ ( 𝑍 × 𝑍 ) ) ) ⊆ ( 𝐶 ∪ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) )
97 86 95 96 syl2anc ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 1st ‘ ( 1st𝑥 ) ) ∖ ( 𝑍 × 𝑍 ) ) ) ⊆ ( 𝐶 ∪ ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ) )
98 inundif ( ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 1st ‘ ( 1st𝑥 ) ) ∖ ( 𝑍 × 𝑍 ) ) ) = ( 1st ‘ ( 1st𝑥 ) )
99 98 eqcomi ( 1st ‘ ( 1st𝑥 ) ) = ( ( ( 1st ‘ ( 1st𝑥 ) ) ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 1st ‘ ( 1st𝑥 ) ) ∖ ( 𝑍 × 𝑍 ) ) )
100 97 99 7 3sstr4g ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( 1st ‘ ( 1st𝑥 ) ) ⊆ 𝑀 )
101 ssidd ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝐻𝐻 )
102 4 12 47 48 49 51 100 101 ss2mcls ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ( ( 1st ‘ ( 1st𝑥 ) ) ( mCls ‘ 𝑇 ) 𝐻 ) ⊆ ( 𝑀 ( mCls ‘ 𝑇 ) 𝐻 ) )
103 89 53 eqeltrrd ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → ⟨ ( 1st ‘ ( 1st𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ 𝐽 )
104 8 2 47 elmpps ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ↔ ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) ∧ 𝐴 ∈ ( ( 1st ‘ ( 1st𝑥 ) ) ( mCls ‘ 𝑇 ) 𝐻 ) ) )
105 104 simprbi ( ⟨ ( 1st ‘ ( 1st𝑥 ) ) , 𝐻 , 𝐴 ⟩ ∈ 𝐽𝐴 ∈ ( ( 1st ‘ ( 1st𝑥 ) ) ( mCls ‘ 𝑇 ) 𝐻 ) )
106 103 105 syl ( ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) ∧ ( 𝑥𝐽 ∧ ( 𝑅𝑥 ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) → 𝐴 ∈ ( ( 1st ‘ ( 1st𝑥 ) ) ( 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 disjdifr ( ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ∩ ( 𝑍 × 𝑍 ) ) = ∅
114 0ss ∅ ⊆ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) )
115 113 114 eqsstri ( ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ∩ ( 𝑍 × 𝑍 ) ) ⊆ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) )
116 ssequn2 ( ( ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ∩ ( 𝑍 × 𝑍 ) ) ⊆ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) ↔ ( ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ∩ ( 𝑍 × 𝑍 ) ) ) = ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) )
117 115 116 mpbi ( ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) ∪ ( ( 𝐷 ∖ ( 𝑍 × 𝑍 ) ) ∩ ( 𝑍 × 𝑍 ) ) ) = ( 𝐶 ∩ ( 𝑍 × 𝑍 ) )
118 111 112 117 3eqtri ( 𝑀 ∩ ( 𝑍 × 𝑍 ) ) = ( 𝐶 ∩ ( 𝑍 × 𝑍 ) )
119 118 a1i ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝑀 ∩ ( 𝑍 × 𝑍 ) ) = ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) )
120 119 oteq1d ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ⟨ ( 𝑀 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ = ⟨ ( 𝐶 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
121 5 8 1 6 msrval ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ ( mPreSt ‘ 𝑇 ) → ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝑀 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
122 44 121 syl ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ⟨ ( 𝑀 ∩ ( 𝑍 × 𝑍 ) ) , 𝐻 , 𝐴 ⟩ )
123 120 122 65 3eqtr4d ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) )
124 110 123 jca ( ( 𝑇 ∈ mFS ∧ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ) → ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ∧ ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) )
125 124 ex ( 𝑇 ∈ mFS → ( ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 → ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ∧ ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) )
126 1 2 3 mthmi ( ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ∧ ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) → ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 )
127 125 126 impbid1 ( 𝑇 ∈ mFS → ( ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ∈ 𝑈 ↔ ( ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ∈ 𝐽 ∧ ( 𝑅 ‘ ⟨ 𝑀 , 𝐻 , 𝐴 ⟩ ) = ( 𝑅 ‘ ⟨ 𝐶 , 𝐻 , 𝐴 ⟩ ) ) ) )