frege133

Description: If the procedure R is single-valued and if M and Y follow X in the R -sequence, then Y belongs to the R -sequence beginning with M or precedes M in the R -sequence. Proposition 133 of Frege1879 p. 86. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege133.x	$⊢ X \in U$
	frege133.y	$⊢ Y \in V$
	frege133.m	$⊢ M \in W$
	frege133.r	$⊢ R \in S$
Assertion	frege133	$⊢ Fun {R^{-1}}^{-1} \to (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y)))$

Proof

Step	Hyp	Ref	Expression
1		frege133.x	$⊢ X \in U$
2		frege133.y	$⊢ Y \in V$
3		frege133.m	$⊢ M \in W$
4		frege133.r	$⊢ R \in S$
5		fvex	$⊢ t+ (R) \in V$
6	5	cnvex	$⊢ {t+ (R)}^{-1} \in V$
7		imaexg	$⊢ {t+ (R)}^{-1} \in V \to {t+ (R)}^{-1} [\{M\}] \in V$
8	6 7	ax-mp	$⊢ {t+ (R)}^{-1} [\{M\}] \in V$
9		imaundir	$⊢ (t+ (R) \cup I) [\{M\}] = t+ (R) [\{M\}] \cup I [\{M\}]$
10		imaexg	$⊢ t+ (R) \in V \to t+ (R) [\{M\}] \in V$
11	5 10	ax-mp	$⊢ t+ (R) [\{M\}] \in V$
12		imai	$⊢ I [\{M\}] = \{M\}$
13		snex	$⊢ \{M\} \in V$
14	12 13	eqeltri	$⊢ I [\{M\}] \in V$
15	11 14	unex	$⊢ t+ (R) [\{M\}] \cup I [\{M\}] \in V$
16	9 15	eqeltri	$⊢ (t+ (R) \cup I) [\{M\}] \in V$
17	1 2 4 8 16	frege83	$⊢ R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to (X \in {t+ (R)}^{-1} [\{M\}] \to (X t+ (R) Y \to Y \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])))$
18	3	elexi	$⊢ M \in V$
19	1	elexi	$⊢ X \in V$
20	18 19	elimasn	$⊢ X \in {t+ (R)}^{-1} [\{M\}] \leftrightarrow ⟨M, X⟩ \in {t+ (R)}^{-1}$
21		df-br	$⊢ M {t+ (R)}^{-1} X \leftrightarrow ⟨M, X⟩ \in {t+ (R)}^{-1}$
22	18 19	brcnv	$⊢ M {t+ (R)}^{-1} X \leftrightarrow X t+ (R) M$
23	20 21 22	3bitr2i	$⊢ X \in {t+ (R)}^{-1} [\{M\}] \leftrightarrow X t+ (R) M$
24		elun	$⊢ Y \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \leftrightarrow (Y \in {t+ (R)}^{-1} [\{M\}] \lor Y \in (t+ (R) \cup I) [\{M\}])$
25		df-or	$⊢ (Y \in {t+ (R)}^{-1} [\{M\}] \lor Y \in (t+ (R) \cup I) [\{M\}]) \leftrightarrow (\neg Y \in {t+ (R)}^{-1} [\{M\}] \to Y \in (t+ (R) \cup I) [\{M\}])$
26	2	elexi	$⊢ Y \in V$
27	18 26	elimasn	$⊢ Y \in {t+ (R)}^{-1} [\{M\}] \leftrightarrow ⟨M, Y⟩ \in {t+ (R)}^{-1}$
28		df-br	$⊢ M {t+ (R)}^{-1} Y \leftrightarrow ⟨M, Y⟩ \in {t+ (R)}^{-1}$
29	18 26	brcnv	$⊢ M {t+ (R)}^{-1} Y \leftrightarrow Y t+ (R) M$
30	27 28 29	3bitr2i	$⊢ Y \in {t+ (R)}^{-1} [\{M\}] \leftrightarrow Y t+ (R) M$
31	30	notbii	$⊢ \neg Y \in {t+ (R)}^{-1} [\{M\}] \leftrightarrow \neg Y t+ (R) M$
32	18 26	elimasn	$⊢ Y \in (t+ (R) \cup I) [\{M\}] \leftrightarrow ⟨M, Y⟩ \in (t+ (R) \cup I)$
33		df-br	$⊢ M (t+ (R) \cup I) Y \leftrightarrow ⟨M, Y⟩ \in (t+ (R) \cup I)$
34	32 33	bitr4i	$⊢ Y \in (t+ (R) \cup I) [\{M\}] \leftrightarrow M (t+ (R) \cup I) Y$
35	31 34	imbi12i	$⊢ (\neg Y \in {t+ (R)}^{-1} [\{M\}] \to Y \in (t+ (R) \cup I) [\{M\}]) \leftrightarrow (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y)$
36	24 25 35	3bitri	$⊢ Y \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \leftrightarrow (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y)$
37	36	imbi2i	$⊢ (X t+ (R) Y \to Y \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])) \leftrightarrow (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y))$
38	23 37	imbi12i	$⊢ (X \in {t+ (R)}^{-1} [\{M\}] \to (X t+ (R) Y \to Y \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]))) \leftrightarrow (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y)))$
39	38	imbi2i	$⊢ (R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to (X \in {t+ (R)}^{-1} [\{M\}] \to (X t+ (R) Y \to Y \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])))) \leftrightarrow (R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y))))$
40	3 4	frege132	$⊢ (R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y)))) \to (Fun {R^{-1}}^{-1} \to (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y))))$
41	39 40	sylbi	$⊢ (R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to (X \in {t+ (R)}^{-1} [\{M\}] \to (X t+ (R) Y \to Y \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])))) \to (Fun {R^{-1}}^{-1} \to (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y))))$
42	17 41	ax-mp	$⊢ Fun {R^{-1}}^{-1} \to (X t+ (R) M \to (X t+ (R) Y \to (\neg Y t+ (R) M \to M (t+ (R) \cup I) Y)))$

Metamath Proof Explorer

Theorem frege133

Proof