frminOLD

Description: Obsolete proof of frmin as of 27-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 4-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	frminOLD	$⊢ ((R Fr A \land R Se A) \land (B \subseteq A \land B \neq \emptyset)) \to \exists y \in B Pred (R, B, y) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		frss	$⊢ B \subseteq A \to (R Fr A \to R Fr B)$
2		sess2	$⊢ B \subseteq A \to (R Se A \to R Se B)$
3	1 2	anim12d	$⊢ B \subseteq A \to ((R Fr A \land R Se A) \to (R Fr B \land R Se B))$
4		n0	$⊢ B \neq \emptyset \leftrightarrow \exists b b \in B$
5		predeq3	$⊢ y = b \to Pred (R, B, y) = Pred (R, B, b)$
6	5	eqeq1d	$⊢ y = b \to (Pred (R, B, y) = \emptyset \leftrightarrow Pred (R, B, b) = \emptyset)$
7	6	rspcev	$⊢ (b \in B \land Pred (R, B, b) = \emptyset) \to \exists y \in B Pred (R, B, y) = \emptyset$
8	7	ex	$⊢ b \in B \to (Pred (R, B, b) = \emptyset \to \exists y \in B Pred (R, B, y) = \emptyset)$
9	8	adantl	$⊢ ((R Fr B \land R Se B) \land b \in B) \to (Pred (R, B, b) = \emptyset \to \exists y \in B Pred (R, B, y) = \emptyset)$
10		setlikespec	$⊢ (b \in B \land R Se B) \to Pred (R, B, b) \in V$
11		trpredpred	$⊢ Pred (R, B, b) \in V \to Pred (R, B, b) \subseteq TrPred (R, B, b)$
12		ssn0	$⊢ (Pred (R, B, b) \subseteq TrPred (R, B, b) \land Pred (R, B, b) \neq \emptyset) \to TrPred (R, B, b) \neq \emptyset$
13	12	ex	$⊢ Pred (R, B, b) \subseteq TrPred (R, B, b) \to (Pred (R, B, b) \neq \emptyset \to TrPred (R, B, b) \neq \emptyset)$
14	11 13	syl	$⊢ Pred (R, B, b) \in V \to (Pred (R, B, b) \neq \emptyset \to TrPred (R, B, b) \neq \emptyset)$
15		trpredss	$⊢ Pred (R, B, b) \in V \to TrPred (R, B, b) \subseteq B$
16	14 15	jctild	$⊢ Pred (R, B, b) \in V \to (Pred (R, B, b) \neq \emptyset \to (TrPred (R, B, b) \subseteq B \land TrPred (R, B, b) \neq \emptyset))$
17	10 16	syl	$⊢ (b \in B \land R Se B) \to (Pred (R, B, b) \neq \emptyset \to (TrPred (R, B, b) \subseteq B \land TrPred (R, B, b) \neq \emptyset))$
18	17	adantr	$⊢ ((b \in B \land R Se B) \land R Fr B) \to (Pred (R, B, b) \neq \emptyset \to (TrPred (R, B, b) \subseteq B \land TrPred (R, B, b) \neq \emptyset))$
19		trpredex	$⊢ TrPred (R, B, b) \in V$
20		sseq1	$⊢ c = TrPred (R, B, b) \to (c \subseteq B \leftrightarrow TrPred (R, B, b) \subseteq B)$
21		neeq1	$⊢ c = TrPred (R, B, b) \to (c \neq \emptyset \leftrightarrow TrPred (R, B, b) \neq \emptyset)$
22	20 21	anbi12d	$⊢ c = TrPred (R, B, b) \to ((c \subseteq B \land c \neq \emptyset) \leftrightarrow (TrPred (R, B, b) \subseteq B \land TrPred (R, B, b) \neq \emptyset))$
23		predeq2	$⊢ c = TrPred (R, B, b) \to Pred (R, c, y) = Pred (R, TrPred (R, B, b), y)$
24	23	eqeq1d	$⊢ c = TrPred (R, B, b) \to (Pred (R, c, y) = \emptyset \leftrightarrow Pred (R, TrPred (R, B, b), y) = \emptyset)$
25	24	rexeqbi1dv	$⊢ c = TrPred (R, B, b) \to (\exists y \in c Pred (R, c, y) = \emptyset \leftrightarrow \exists y \in TrPred (R, B, b) Pred (R, TrPred (R, B, b), y) = \emptyset)$
26	22 25	imbi12d	$⊢ c = TrPred (R, B, b) \to (((c \subseteq B \land c \neq \emptyset) \to \exists y \in c Pred (R, c, y) = \emptyset) \leftrightarrow ((TrPred (R, B, b) \subseteq B \land TrPred (R, B, b) \neq \emptyset) \to \exists y \in TrPred (R, B, b) Pred (R, TrPred (R, B, b), y) = \emptyset))$
27	26	imbi2d	$⊢ c = TrPred (R, B, b) \to ((R Fr B \to ((c \subseteq B \land c \neq \emptyset) \to \exists y \in c Pred (R, c, y) = \emptyset)) \leftrightarrow (R Fr B \to ((TrPred (R, B, b) \subseteq B \land TrPred (R, B, b) \neq \emptyset) \to \exists y \in TrPred (R, B, b) Pred (R, TrPred (R, B, b), y) = \emptyset)))$
28		dffr4	$⊢ R Fr B \leftrightarrow \forall c ((c \subseteq B \land c \neq \emptyset) \to \exists y \in c Pred (R, c, y) = \emptyset)$
29		sp	$⊢ \forall c ((c \subseteq B \land c \neq \emptyset) \to \exists y \in c Pred (R, c, y) = \emptyset) \to ((c \subseteq B \land c \neq \emptyset) \to \exists y \in c Pred (R, c, y) = \emptyset)$
30	28 29	sylbi	$⊢ R Fr B \to ((c \subseteq B \land c \neq \emptyset) \to \exists y \in c Pred (R, c, y) = \emptyset)$
31	19 27 30	vtocl	$⊢ R Fr B \to ((TrPred (R, B, b) \subseteq B \land TrPred (R, B, b) \neq \emptyset) \to \exists y \in TrPred (R, B, b) Pred (R, TrPred (R, B, b), y) = \emptyset)$
32	10 15	syl	$⊢ (b \in B \land R Se B) \to TrPred (R, B, b) \subseteq B$
33	32	adantr	$⊢ ((b \in B \land R Se B) \land y \in TrPred (R, B, b)) \to TrPred (R, B, b) \subseteq B$
34		trpredtr	$⊢ (b \in B \land R Se B) \to (y \in TrPred (R, B, b) \to Pred (R, B, y) \subseteq TrPred (R, B, b))$
35	34	imp	$⊢ ((b \in B \land R Se B) \land y \in TrPred (R, B, b)) \to Pred (R, B, y) \subseteq TrPred (R, B, b)$
36		sspred	$⊢ (TrPred (R, B, b) \subseteq B \land Pred (R, B, y) \subseteq TrPred (R, B, b)) \to Pred (R, B, y) = Pred (R, TrPred (R, B, b), y)$
37	33 35 36	syl2anc	$⊢ ((b \in B \land R Se B) \land y \in TrPred (R, B, b)) \to Pred (R, B, y) = Pred (R, TrPred (R, B, b), y)$
38	37	eqeq1d	$⊢ ((b \in B \land R Se B) \land y \in TrPred (R, B, b)) \to (Pred (R, B, y) = \emptyset \leftrightarrow Pred (R, TrPred (R, B, b), y) = \emptyset)$
39	38	biimprd	$⊢ ((b \in B \land R Se B) \land y \in TrPred (R, B, b)) \to (Pred (R, TrPred (R, B, b), y) = \emptyset \to Pred (R, B, y) = \emptyset)$
40	39	reximdva	$⊢ (b \in B \land R Se B) \to (\exists y \in TrPred (R, B, b) Pred (R, TrPred (R, B, b), y) = \emptyset \to \exists y \in TrPred (R, B, b) Pred (R, B, y) = \emptyset)$
41		ssrexv	$⊢ TrPred (R, B, b) \subseteq B \to (\exists y \in TrPred (R, B, b) Pred (R, B, y) = \emptyset \to \exists y \in B Pred (R, B, y) = \emptyset)$
42	32 40 41	sylsyld	$⊢ (b \in B \land R Se B) \to (\exists y \in TrPred (R, B, b) Pred (R, TrPred (R, B, b), y) = \emptyset \to \exists y \in B Pred (R, B, y) = \emptyset)$
43	31 42	sylan9r	$⊢ ((b \in B \land R Se B) \land R Fr B) \to ((TrPred (R, B, b) \subseteq B \land TrPred (R, B, b) \neq \emptyset) \to \exists y \in B Pred (R, B, y) = \emptyset)$
44	18 43	syld	$⊢ ((b \in B \land R Se B) \land R Fr B) \to (Pred (R, B, b) \neq \emptyset \to \exists y \in B Pred (R, B, y) = \emptyset)$
45	44	an31s	$⊢ ((R Fr B \land R Se B) \land b \in B) \to (Pred (R, B, b) \neq \emptyset \to \exists y \in B Pred (R, B, y) = \emptyset)$
46	9 45	pm2.61dne	$⊢ ((R Fr B \land R Se B) \land b \in B) \to \exists y \in B Pred (R, B, y) = \emptyset$
47	46	ex	$⊢ (R Fr B \land R Se B) \to (b \in B \to \exists y \in B Pred (R, B, y) = \emptyset)$
48	47	exlimdv	$⊢ (R Fr B \land R Se B) \to (\exists b b \in B \to \exists y \in B Pred (R, B, y) = \emptyset)$
49	4 48	syl5bi	$⊢ (R Fr B \land R Se B) \to (B \neq \emptyset \to \exists y \in B Pred (R, B, y) = \emptyset)$
50	3 49	syl6com	$⊢ (R Fr A \land R Se A) \to (B \subseteq A \to (B \neq \emptyset \to \exists y \in B Pred (R, B, y) = \emptyset))$
51	50	imp32	$⊢ ((R Fr A \land R Se A) \land (B \subseteq A \land B \neq \emptyset)) \to \exists y \in B Pred (R, B, y) = \emptyset$

Metamath Proof Explorer

Theorem frminOLD

Proof