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	$⊢ R = mStRed (T)$
	mthmpps.j	$⊢ J = mPPSt (T)$
	mthmpps.u	$⊢ U = mThm (T)$
	mthmpps.d	$⊢ D = mDV (T)$
	mthmpps.v	$⊢ V = mVars (T)$
	mthmpps.z	$⊢ Z = ⋃ V [H \cup \{A\}]$
	mthmpps.m	$⊢ M = C \cup (D ∖ (Z \times Z))$
Assertion	mthmpps	$⊢ T \in mFS \to (⟨C, H, A⟩ \in U \leftrightarrow (⟨M, H, A⟩ \in J \land R (⟨M, H, A⟩) = R (⟨C, H, A⟩)))$

Proof

Step	Hyp	Ref	Expression
1		mthmpps.r	$⊢ R = mStRed (T)$
2		mthmpps.j	$⊢ J = mPPSt (T)$
3		mthmpps.u	$⊢ U = mThm (T)$
4		mthmpps.d	$⊢ D = mDV (T)$
5		mthmpps.v	$⊢ V = mVars (T)$
6		mthmpps.z	$⊢ Z = ⋃ V [H \cup \{A\}]$
7		mthmpps.m	$⊢ M = C \cup (D ∖ (Z \times Z))$
8		eqid	$⊢ mPreSt (T) = mPreSt (T)$
9	3 8	mthmsta	$⊢ U \subseteq mPreSt (T)$
10		simpr	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to ⟨C, H, A⟩ \in U$
11	9 10	sseldi	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to ⟨C, H, A⟩ \in mPreSt (T)$
12		eqid	$⊢ mEx (T) = mEx (T)$
13	4 12 8	elmpst	$⊢ ⟨C, H, A⟩ \in mPreSt (T) \leftrightarrow ((C \subseteq D \land C^{-1} = C) \land (H \subseteq mEx (T) \land H \in Fin) \land A \in mEx (T))$
14	11 13	sylib	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to ((C \subseteq D \land C^{-1} = C) \land (H \subseteq mEx (T) \land H \in Fin) \land A \in mEx (T))$
15	14	simp1d	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to (C \subseteq D \land C^{-1} = C)$
16	15	simpld	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to C \subseteq D$
17		difssd	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to D ∖ (Z \times Z) \subseteq D$
18	16 17	unssd	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to C \cup (D ∖ (Z \times Z)) \subseteq D$
19	7 18	eqsstrid	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to M \subseteq D$
20	15	simprd	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to C^{-1} = C$
21		cnvdif	$⊢ {(D ∖ (Z \times Z))}^{-1} = D^{-1} ∖ {(Z \times Z)}^{-1}$
22		cnvdif	$⊢ {((mVR (T) \times mVR (T)) ∖ I)}^{-1} = {(mVR (T) \times mVR (T))}^{-1} ∖ I^{-1}$
23		cnvxp	$⊢ {(mVR (T) \times mVR (T))}^{-1} = mVR (T) \times mVR (T)$
24		cnvi	$⊢ I^{-1} = I$
25	23 24	difeq12i	$⊢ {(mVR (T) \times mVR (T))}^{-1} ∖ I^{-1} = (mVR (T) \times mVR (T)) ∖ I$
26	22 25	eqtri	$⊢ {((mVR (T) \times mVR (T)) ∖ I)}^{-1} = (mVR (T) \times mVR (T)) ∖ I$
27		eqid	$⊢ mVR (T) = mVR (T)$
28	27 4	mdvval	$⊢ D = (mVR (T) \times mVR (T)) ∖ I$
29	28	cnveqi	$⊢ D^{-1} = {((mVR (T) \times mVR (T)) ∖ I)}^{-1}$
30	26 29 28	3eqtr4i	$⊢ D^{-1} = D$
31		cnvxp	$⊢ {(Z \times Z)}^{-1} = Z \times Z$
32	30 31	difeq12i	$⊢ D^{-1} ∖ {(Z \times Z)}^{-1} = D ∖ (Z \times Z)$
33	21 32	eqtri	$⊢ {(D ∖ (Z \times Z))}^{-1} = D ∖ (Z \times Z)$
34	33	a1i	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to {(D ∖ (Z \times Z))}^{-1} = D ∖ (Z \times Z)$
35	20 34	uneq12d	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to C^{-1} \cup {(D ∖ (Z \times Z))}^{-1} = C \cup (D ∖ (Z \times Z))$
36	7	cnveqi	$⊢ M^{-1} = {(C \cup (D ∖ (Z \times Z)))}^{-1}$
37		cnvun	$⊢ {(C \cup (D ∖ (Z \times Z)))}^{-1} = C^{-1} \cup {(D ∖ (Z \times Z))}^{-1}$
38	36 37	eqtri	$⊢ M^{-1} = C^{-1} \cup {(D ∖ (Z \times Z))}^{-1}$
39	35 38 7	3eqtr4g	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to M^{-1} = M$
40	19 39	jca	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to (M \subseteq D \land M^{-1} = M)$
41	14	simp2d	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to (H \subseteq mEx (T) \land H \in Fin)$
42	14	simp3d	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to A \in mEx (T)$
43	4 12 8	elmpst	$⊢ ⟨M, H, A⟩ \in mPreSt (T) \leftrightarrow ((M \subseteq D \land M^{-1} = M) \land (H \subseteq mEx (T) \land H \in Fin) \land A \in mEx (T))$
44	40 41 42 43	syl3anbrc	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to ⟨M, H, A⟩ \in mPreSt (T)$
45	1 2 3	elmthm	$⊢ ⟨C, H, A⟩ \in U \leftrightarrow \exists x \in J R (x) = R (⟨C, H, A⟩)$
46	10 45	sylib	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to \exists x \in J R (x) = R (⟨C, H, A⟩)$
47		eqid	$⊢ mCls (T) = mCls (T)$
48		simpll	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to T \in mFS$
49	19	adantr	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to M \subseteq D$
50	41	simpld	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to H \subseteq mEx (T)$
51	50	adantr	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to H \subseteq mEx (T)$
52	8 2	mppspst	$⊢ J \subseteq mPreSt (T)$
53		simprl	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to x \in J$
54	52 53	sseldi	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to x \in mPreSt (T)$
55	8	mpst123	$⊢ x \in mPreSt (T) \to x = ⟨1^{st} (1^{st} (x)), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩$
56	54 55	syl	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to x = ⟨1^{st} (1^{st} (x)), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩$
57	56	fveq2d	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to R (x) = R (⟨1^{st} (1^{st} (x)), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩)$
58		simprr	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to R (x) = R (⟨C, H, A⟩)$
59	57 58	eqtr3d	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to R (⟨1^{st} (1^{st} (x)), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩) = R (⟨C, H, A⟩)$
60	56 54	eqeltrrd	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to ⟨1^{st} (1^{st} (x)), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩ \in mPreSt (T)$
61		eqid	$⊢ ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] = ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}]$
62	5 8 1 61	msrval	$⊢ ⟨1^{st} (1^{st} (x)), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩ \in mPreSt (T) \to R (⟨1^{st} (1^{st} (x)), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩) = ⟨1^{st} (1^{st} (x)) \cap (⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] \times ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}]), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩$
63	60 62	syl	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to R (⟨1^{st} (1^{st} (x)), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩) = ⟨1^{st} (1^{st} (x)) \cap (⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] \times ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}]), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩$
64	5 8 1 6	msrval	$⊢ ⟨C, H, A⟩ \in mPreSt (T) \to R (⟨C, H, A⟩) = ⟨C \cap (Z \times Z), H, A⟩$
65	11 64	syl	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to R (⟨C, H, A⟩) = ⟨C \cap (Z \times Z), H, A⟩$
66	65	adantr	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to R (⟨C, H, A⟩) = ⟨C \cap (Z \times Z), H, A⟩$
67	59 63 66	3eqtr3d	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to ⟨1^{st} (1^{st} (x)) \cap (⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] \times ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}]), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩ = ⟨C \cap (Z \times Z), H, A⟩$
68		fvex	$⊢ 1^{st} (1^{st} (x)) \in V$
69	68	inex1	$⊢ 1^{st} (1^{st} (x)) \cap (⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] \times ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}]) \in V$
70		fvex	$⊢ 2^{nd} (1^{st} (x)) \in V$
71		fvex	$⊢ 2^{nd} (x) \in V$
72	69 70 71	otth	$⊢ ⟨1^{st} (1^{st} (x)) \cap (⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] \times ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}]), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩ = ⟨C \cap (Z \times Z), H, A⟩ \leftrightarrow (1^{st} (1^{st} (x)) \cap (⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] \times ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}]) = C \cap (Z \times Z) \land 2^{nd} (1^{st} (x)) = H \land 2^{nd} (x) = A)$
73	67 72	sylib	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to (1^{st} (1^{st} (x)) \cap (⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] \times ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}]) = C \cap (Z \times Z) \land 2^{nd} (1^{st} (x)) = H \land 2^{nd} (x) = A)$
74	73	simp1d	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to 1^{st} (1^{st} (x)) \cap (⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] \times ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}]) = C \cap (Z \times Z)$
75	73	simp2d	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to 2^{nd} (1^{st} (x)) = H$
76	73	simp3d	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to 2^{nd} (x) = A$
77	76	sneqd	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to \{2^{nd} (x)\} = \{A\}$
78	75 77	uneq12d	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to 2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\} = H \cup \{A\}$
79	78	imaeq2d	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] = V [H \cup \{A\}]$
80	79	unieqd	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] = ⋃ V [H \cup \{A\}]$
81	80 6	eqtr4di	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] = Z$
82	81	sqxpeqd	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] \times ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] = Z \times Z$
83	82	ineq2d	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to 1^{st} (1^{st} (x)) \cap (⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}] \times ⋃ V [2^{nd} (1^{st} (x)) \cup \{2^{nd} (x)\}]) = 1^{st} (1^{st} (x)) \cap (Z \times Z)$
84	74 83	eqtr3d	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to C \cap (Z \times Z) = 1^{st} (1^{st} (x)) \cap (Z \times Z)$
85		inss1	$⊢ C \cap (Z \times Z) \subseteq C$
86	84 85	eqsstrrdi	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to 1^{st} (1^{st} (x)) \cap (Z \times Z) \subseteq C$
87		eqidd	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to 1^{st} (1^{st} (x)) = 1^{st} (1^{st} (x))$
88	87 75 76	oteq123d	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to ⟨1^{st} (1^{st} (x)), 2^{nd} (1^{st} (x)), 2^{nd} (x)⟩ = ⟨1^{st} (1^{st} (x)), H, A⟩$
89	56 88	eqtrd	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to x = ⟨1^{st} (1^{st} (x)), H, A⟩$
90	89 54	eqeltrrd	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to ⟨1^{st} (1^{st} (x)), H, A⟩ \in mPreSt (T)$
91	4 12 8	elmpst	$⊢ ⟨1^{st} (1^{st} (x)), H, A⟩ \in mPreSt (T) \leftrightarrow ((1^{st} (1^{st} (x)) \subseteq D \land {1^{st} (1^{st} (x))}^{-1} = 1^{st} (1^{st} (x))) \land (H \subseteq mEx (T) \land H \in Fin) \land A \in mEx (T))$
92	91	simp1bi	$⊢ ⟨1^{st} (1^{st} (x)), H, A⟩ \in mPreSt (T) \to (1^{st} (1^{st} (x)) \subseteq D \land {1^{st} (1^{st} (x))}^{-1} = 1^{st} (1^{st} (x)))$
93	92	simpld	$⊢ ⟨1^{st} (1^{st} (x)), H, A⟩ \in mPreSt (T) \to 1^{st} (1^{st} (x)) \subseteq D$
94	90 93	syl	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to 1^{st} (1^{st} (x)) \subseteq D$
95	94	ssdifd	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to 1^{st} (1^{st} (x)) ∖ (Z \times Z) \subseteq D ∖ (Z \times Z)$
96		unss12	$⊢ (1^{st} (1^{st} (x)) \cap (Z \times Z) \subseteq C \land 1^{st} (1^{st} (x)) ∖ (Z \times Z) \subseteq D ∖ (Z \times Z)) \to (1^{st} (1^{st} (x)) \cap (Z \times Z)) \cup (1^{st} (1^{st} (x)) ∖ (Z \times Z)) \subseteq C \cup (D ∖ (Z \times Z))$
97	86 95 96	syl2anc	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to (1^{st} (1^{st} (x)) \cap (Z \times Z)) \cup (1^{st} (1^{st} (x)) ∖ (Z \times Z)) \subseteq C \cup (D ∖ (Z \times Z))$
98		inundif	$⊢ (1^{st} (1^{st} (x)) \cap (Z \times Z)) \cup (1^{st} (1^{st} (x)) ∖ (Z \times Z)) = 1^{st} (1^{st} (x))$
99	98	eqcomi	$⊢ 1^{st} (1^{st} (x)) = (1^{st} (1^{st} (x)) \cap (Z \times Z)) \cup (1^{st} (1^{st} (x)) ∖ (Z \times Z))$
100	97 99 7	3sstr4g	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to 1^{st} (1^{st} (x)) \subseteq M$
101		ssidd	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to H \subseteq H$
102	4 12 47 48 49 51 100 101	ss2mcls	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to 1^{st} (1^{st} (x)) mCls (T) H \subseteq M mCls (T) H$
103	89 53	eqeltrrd	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to ⟨1^{st} (1^{st} (x)), H, A⟩ \in J$
104	8 2 47	elmpps	$⊢ ⟨1^{st} (1^{st} (x)), H, A⟩ \in J \leftrightarrow (⟨1^{st} (1^{st} (x)), H, A⟩ \in mPreSt (T) \land A \in (1^{st} (1^{st} (x)) mCls (T) H))$
105	104	simprbi	$⊢ ⟨1^{st} (1^{st} (x)), H, A⟩ \in J \to A \in (1^{st} (1^{st} (x)) mCls (T) H)$
106	103 105	syl	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to A \in (1^{st} (1^{st} (x)) mCls (T) H)$
107	102 106	sseldd	$⊢ ((T \in mFS \land ⟨C, H, A⟩ \in U) \land (x \in J \land R (x) = R (⟨C, H, A⟩))) \to A \in (M mCls (T) H)$
108	46 107	rexlimddv	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to A \in (M mCls (T) H)$
109	8 2 47	elmpps	$⊢ ⟨M, H, A⟩ \in J \leftrightarrow (⟨M, H, A⟩ \in mPreSt (T) \land A \in (M mCls (T) H))$
110	44 108 109	sylanbrc	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to ⟨M, H, A⟩ \in J$
111	7	ineq1i	$⊢ M \cap (Z \times Z) = (C \cup (D ∖ (Z \times Z))) \cap (Z \times Z)$
112		indir	$⊢ (C \cup (D ∖ (Z \times Z))) \cap (Z \times Z) = (C \cap (Z \times Z)) \cup ((D ∖ (Z \times Z)) \cap (Z \times Z))$
113		disjdifr	$⊢ (D ∖ (Z \times Z)) \cap (Z \times Z) = \emptyset$
114		0ss	$⊢ \emptyset \subseteq C \cap (Z \times Z)$
115	113 114	eqsstri	$⊢ (D ∖ (Z \times Z)) \cap (Z \times Z) \subseteq C \cap (Z \times Z)$
116		ssequn2	$⊢ (D ∖ (Z \times Z)) \cap (Z \times Z) \subseteq C \cap (Z \times Z) \leftrightarrow (C \cap (Z \times Z)) \cup ((D ∖ (Z \times Z)) \cap (Z \times Z)) = C \cap (Z \times Z)$
117	115 116	mpbi	$⊢ (C \cap (Z \times Z)) \cup ((D ∖ (Z \times Z)) \cap (Z \times Z)) = C \cap (Z \times Z)$
118	111 112 117	3eqtri	$⊢ M \cap (Z \times Z) = C \cap (Z \times Z)$
119	118	a1i	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to M \cap (Z \times Z) = C \cap (Z \times Z)$
120	119	oteq1d	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to ⟨M \cap (Z \times Z), H, A⟩ = ⟨C \cap (Z \times Z), H, A⟩$
121	5 8 1 6	msrval	$⊢ ⟨M, H, A⟩ \in mPreSt (T) \to R (⟨M, H, A⟩) = ⟨M \cap (Z \times Z), H, A⟩$
122	44 121	syl	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to R (⟨M, H, A⟩) = ⟨M \cap (Z \times Z), H, A⟩$
123	120 122 65	3eqtr4d	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to R (⟨M, H, A⟩) = R (⟨C, H, A⟩)$
124	110 123	jca	$⊢ (T \in mFS \land ⟨C, H, A⟩ \in U) \to (⟨M, H, A⟩ \in J \land R (⟨M, H, A⟩) = R (⟨C, H, A⟩))$
125	124	ex	$⊢ T \in mFS \to (⟨C, H, A⟩ \in U \to (⟨M, H, A⟩ \in J \land R (⟨M, H, A⟩) = R (⟨C, H, A⟩)))$
126	1 2 3	mthmi	$⊢ (⟨M, H, A⟩ \in J \land R (⟨M, H, A⟩) = R (⟨C, H, A⟩)) \to ⟨C, H, A⟩ \in U$
127	125 126	impbid1	$⊢ T \in mFS \to (⟨C, H, A⟩ \in U \leftrightarrow (⟨M, H, A⟩ \in J \land R (⟨M, H, A⟩) = R (⟨C, H, A⟩)))$

Metamath Proof Explorer

Theorem mthmpps

Proof