frege131

Description: If the procedure R is single-valued, then the property of belonging to the R -sequence begining with M or preceeding M in the R -sequence is hereditary in the R -sequence. Proposition 131 of Frege1879 p. 85. (Contributed by RP, 9-Jul-2020) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	frege130.m	$⊢ M \in U$
	frege130.r	$⊢ R \in V$
Assertion	frege131	$⊢ Fun {R^{-1}}^{-1} \to R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])$

Proof

Step	Hyp	Ref	Expression
1		frege130.m	$⊢ M \in U$
2		frege130.r	$⊢ R \in V$
3		frege75	$⊢ \forall b (b \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to \forall a (b R a \to a \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]))) \to R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])$
4		elun	$⊢ b \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \leftrightarrow (b \in {t+ (R)}^{-1} [\{M\}] \lor b \in (t+ (R) \cup I) [\{M\}])$
5		df-or	$⊢ (b \in {t+ (R)}^{-1} [\{M\}] \lor b \in (t+ (R) \cup I) [\{M\}]) \leftrightarrow (\neg b \in {t+ (R)}^{-1} [\{M\}] \to b \in (t+ (R) \cup I) [\{M\}])$
6	1	elexi	$⊢ M \in V$
7		vex	$⊢ b \in V$
8	6 7	elimasn	$⊢ b \in {t+ (R)}^{-1} [\{M\}] \leftrightarrow ⟨M, b⟩ \in {t+ (R)}^{-1}$
9		df-br	$⊢ M {t+ (R)}^{-1} b \leftrightarrow ⟨M, b⟩ \in {t+ (R)}^{-1}$
10	6 7	brcnv	$⊢ M {t+ (R)}^{-1} b \leftrightarrow b t+ (R) M$
11	8 9 10	3bitr2i	$⊢ b \in {t+ (R)}^{-1} [\{M\}] \leftrightarrow b t+ (R) M$
12	11	notbii	$⊢ \neg b \in {t+ (R)}^{-1} [\{M\}] \leftrightarrow \neg b t+ (R) M$
13	6 7	elimasn	$⊢ b \in (t+ (R) \cup I) [\{M\}] \leftrightarrow ⟨M, b⟩ \in (t+ (R) \cup I)$
14		df-br	$⊢ M (t+ (R) \cup I) b \leftrightarrow ⟨M, b⟩ \in (t+ (R) \cup I)$
15	13 14	bitr4i	$⊢ b \in (t+ (R) \cup I) [\{M\}] \leftrightarrow M (t+ (R) \cup I) b$
16	12 15	imbi12i	$⊢ (\neg b \in {t+ (R)}^{-1} [\{M\}] \to b \in (t+ (R) \cup I) [\{M\}]) \leftrightarrow (\neg b t+ (R) M \to M (t+ (R) \cup I) b)$
17	4 5 16	3bitri	$⊢ b \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \leftrightarrow (\neg b t+ (R) M \to M (t+ (R) \cup I) b)$
18		elun	$⊢ a \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \leftrightarrow (a \in {t+ (R)}^{-1} [\{M\}] \lor a \in (t+ (R) \cup I) [\{M\}])$
19		df-or	$⊢ (a \in {t+ (R)}^{-1} [\{M\}] \lor a \in (t+ (R) \cup I) [\{M\}]) \leftrightarrow (\neg a \in {t+ (R)}^{-1} [\{M\}] \to a \in (t+ (R) \cup I) [\{M\}])$
20		vex	$⊢ a \in V$
21	6 20	elimasn	$⊢ a \in {t+ (R)}^{-1} [\{M\}] \leftrightarrow ⟨M, a⟩ \in {t+ (R)}^{-1}$
22		df-br	$⊢ M {t+ (R)}^{-1} a \leftrightarrow ⟨M, a⟩ \in {t+ (R)}^{-1}$
23	6 20	brcnv	$⊢ M {t+ (R)}^{-1} a \leftrightarrow a t+ (R) M$
24	21 22 23	3bitr2i	$⊢ a \in {t+ (R)}^{-1} [\{M\}] \leftrightarrow a t+ (R) M$
25	24	notbii	$⊢ \neg a \in {t+ (R)}^{-1} [\{M\}] \leftrightarrow \neg a t+ (R) M$
26	6 20	elimasn	$⊢ a \in (t+ (R) \cup I) [\{M\}] \leftrightarrow ⟨M, a⟩ \in (t+ (R) \cup I)$
27		df-br	$⊢ M (t+ (R) \cup I) a \leftrightarrow ⟨M, a⟩ \in (t+ (R) \cup I)$
28	26 27	bitr4i	$⊢ a \in (t+ (R) \cup I) [\{M\}] \leftrightarrow M (t+ (R) \cup I) a$
29	25 28	imbi12i	$⊢ (\neg a \in {t+ (R)}^{-1} [\{M\}] \to a \in (t+ (R) \cup I) [\{M\}]) \leftrightarrow (\neg a t+ (R) M \to M (t+ (R) \cup I) a)$
30	18 19 29	3bitri	$⊢ a \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \leftrightarrow (\neg a t+ (R) M \to M (t+ (R) \cup I) a)$
31	30	imbi2i	$⊢ (b R a \to a \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])) \leftrightarrow (b R a \to (\neg a t+ (R) M \to M (t+ (R) \cup I) a))$
32	31	albii	$⊢ \forall a (b R a \to a \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])) \leftrightarrow \forall a (b R a \to (\neg a t+ (R) M \to M (t+ (R) \cup I) a))$
33	17 32	imbi12i	$⊢ (b \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to \forall a (b R a \to a \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]))) \leftrightarrow ((\neg b t+ (R) M \to M (t+ (R) \cup I) b) \to \forall a (b R a \to (\neg a t+ (R) M \to M (t+ (R) \cup I) a)))$
34	33	albii	$⊢ \forall b (b \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to \forall a (b R a \to a \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]))) \leftrightarrow \forall b ((\neg b t+ (R) M \to M (t+ (R) \cup I) b) \to \forall a (b R a \to (\neg a t+ (R) M \to M (t+ (R) \cup I) a)))$
35	34	imbi1i	$⊢ (\forall b (b \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to \forall a (b R a \to a \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]))) \to R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])) \leftrightarrow (\forall b ((\neg b t+ (R) M \to M (t+ (R) \cup I) b) \to \forall a (b R a \to (\neg a t+ (R) M \to M (t+ (R) \cup I) a))) \to R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]))$
36	1 2	frege130	$⊢ (\forall b ((\neg b t+ (R) M \to M (t+ (R) \cup I) b) \to \forall a (b R a \to (\neg a t+ (R) M \to M (t+ (R) \cup I) a))) \to R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])) \to (Fun {R^{-1}}^{-1} \to R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]))$
37	35 36	sylbi	$⊢ (\forall b (b \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]) \to \forall a (b R a \to a \in ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]))) \to R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])) \to (Fun {R^{-1}}^{-1} \to R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}]))$
38	3 37	ax-mp	$⊢ Fun {R^{-1}}^{-1} \to R hereditary ({t+ (R)}^{-1} [\{M\}] \cup (t+ (R) \cup I) [\{M\}])$

Metamath Proof Explorer

Theorem frege131

Proof