bnj1417

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1417.1	$⊢ φ \leftrightarrow R FrSe A$
	bnj1417.2	$⊢ ψ \leftrightarrow \neg x \in trCl (x, A, R)$
	bnj1417.3	$⊢ χ \leftrightarrow \forall y \in A (y R x \to \underset{˙}{[} y / x \underset{˙}{]} ψ)$
	bnj1417.4	$⊢ θ \leftrightarrow (φ \land x \in A \land χ)$
	bnj1417.5	$⊢ B = pred (x, A, R) \cup ⋃_{y \in pred (x, A, R)} trCl (y, A, R)$
Assertion	bnj1417	$⊢ φ \to \forall x \in A \neg x \in trCl (x, A, R)$

Proof

Step	Hyp	Ref	Expression
1		bnj1417.1	$⊢ φ \leftrightarrow R FrSe A$
2		bnj1417.2	$⊢ ψ \leftrightarrow \neg x \in trCl (x, A, R)$
3		bnj1417.3	$⊢ χ \leftrightarrow \forall y \in A (y R x \to \underset{˙}{[} y / x \underset{˙}{]} ψ)$
4		bnj1417.4	$⊢ θ \leftrightarrow (φ \land x \in A \land χ)$
5		bnj1417.5	$⊢ B = pred (x, A, R) \cup ⋃_{y \in pred (x, A, R)} trCl (y, A, R)$
6	1	biimpi	$⊢ φ \to R FrSe A$
7		bnj1418	$⊢ x \in pred (x, A, R) \to x R x$
8	7	adantl	$⊢ (θ \land x \in pred (x, A, R)) \to x R x$
9	4 6	bnj835	$⊢ θ \to R FrSe A$
10		df-bnj15	$⊢ R FrSe A \leftrightarrow (R Fr A \land R Se A)$
11	10	simplbi	$⊢ R FrSe A \to R Fr A$
12	9 11	syl	$⊢ θ \to R Fr A$
13		bnj213	$⊢ pred (x, A, R) \subseteq A$
14	13	sseli	$⊢ x \in pred (x, A, R) \to x \in A$
15		frirr	$⊢ (R Fr A \land x \in A) \to \neg x R x$
16	12 14 15	syl2an	$⊢ (θ \land x \in pred (x, A, R)) \to \neg x R x$
17	8 16	pm2.65da	$⊢ θ \to \neg x \in pred (x, A, R)$
18		nfv	$⊢ Ⅎ y φ$
19		nfv	$⊢ Ⅎ y x \in A$
20	3	bnj1095	$⊢ χ \to \forall y χ$
21	20	nf5i	$⊢ Ⅎ y χ$
22	18 19 21	nf3an	$⊢ Ⅎ y (φ \land x \in A \land χ)$
23	4 22	nfxfr	$⊢ Ⅎ y θ$
24	9	ad2antrr	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to R FrSe A$
25		simplr	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to y \in pred (x, A, R)$
26	13 25	sseldi	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to y \in A$
27		simpr	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to x \in trCl (y, A, R)$
28		bnj1125	$⊢ (R FrSe A \land y \in A \land x \in trCl (y, A, R)) \to trCl (x, A, R) \subseteq trCl (y, A, R)$
29	24 26 27 28	syl3anc	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to trCl (x, A, R) \subseteq trCl (y, A, R)$
30		bnj1147	$⊢ trCl (y, A, R) \subseteq A$
31	30 27	sseldi	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to x \in A$
32		bnj906	$⊢ (R FrSe A \land x \in A) \to pred (x, A, R) \subseteq trCl (x, A, R)$
33	24 31 32	syl2anc	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to pred (x, A, R) \subseteq trCl (x, A, R)$
34	33 25	sseldd	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to y \in trCl (x, A, R)$
35	29 34	sseldd	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to y \in trCl (y, A, R)$
36	3	biimpi	$⊢ χ \to \forall y \in A (y R x \to \underset{˙}{[} y / x \underset{˙}{]} ψ)$
37	4 36	bnj837	$⊢ θ \to \forall y \in A (y R x \to \underset{˙}{[} y / x \underset{˙}{]} ψ)$
38	37	ad2antrr	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to \forall y \in A (y R x \to \underset{˙}{[} y / x \underset{˙}{]} ψ)$
39		bnj1418	$⊢ y \in pred (x, A, R) \to y R x$
40	39	ad2antlr	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to y R x$
41		rsp	$⊢ \forall y \in A (y R x \to \underset{˙}{[} y / x \underset{˙}{]} ψ) \to (y \in A \to (y R x \to \underset{˙}{[} y / x \underset{˙}{]} ψ))$
42	38 26 40 41	syl3c	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to \underset{˙}{[} y / x \underset{˙}{]} ψ$
43		vex	$⊢ y \in V$
44		eleq1w	$⊢ x = y \to (x \in trCl (x, A, R) \leftrightarrow y \in trCl (x, A, R))$
45		bnj1318	$⊢ x = y \to trCl (x, A, R) = trCl (y, A, R)$
46	45	eleq2d	$⊢ x = y \to (y \in trCl (x, A, R) \leftrightarrow y \in trCl (y, A, R))$
47	44 46	bitrd	$⊢ x = y \to (x \in trCl (x, A, R) \leftrightarrow y \in trCl (y, A, R))$
48	47	notbid	$⊢ x = y \to (\neg x \in trCl (x, A, R) \leftrightarrow \neg y \in trCl (y, A, R))$
49	2 48	syl5bb	$⊢ x = y \to (ψ \leftrightarrow \neg y \in trCl (y, A, R))$
50	43 49	sbcie	$⊢ \underset{˙}{[} y / x \underset{˙}{]} ψ \leftrightarrow \neg y \in trCl (y, A, R)$
51	42 50	sylib	$⊢ ((θ \land y \in pred (x, A, R)) \land x \in trCl (y, A, R)) \to \neg y \in trCl (y, A, R)$
52	35 51	pm2.65da	$⊢ (θ \land y \in pred (x, A, R)) \to \neg x \in trCl (y, A, R)$
53	52	ex	$⊢ θ \to (y \in pred (x, A, R) \to \neg x \in trCl (y, A, R))$
54	23 53	ralrimi	$⊢ θ \to \forall y \in pred (x, A, R) \neg x \in trCl (y, A, R)$
55		ralnex	$⊢ \forall y \in pred (x, A, R) \neg x \in trCl (y, A, R) \leftrightarrow \neg \exists y \in pred (x, A, R) x \in trCl (y, A, R)$
56	54 55	sylib	$⊢ θ \to \neg \exists y \in pred (x, A, R) x \in trCl (y, A, R)$
57		eliun	$⊢ x \in ⋃_{y \in pred (x, A, R)} trCl (y, A, R) \leftrightarrow \exists y \in pred (x, A, R) x \in trCl (y, A, R)$
58	56 57	sylnibr	$⊢ θ \to \neg x \in ⋃_{y \in pred (x, A, R)} trCl (y, A, R)$
59		ioran	$⊢ \neg (x \in pred (x, A, R) \lor x \in ⋃_{y \in pred (x, A, R)} trCl (y, A, R)) \leftrightarrow (\neg x \in pred (x, A, R) \land \neg x \in ⋃_{y \in pred (x, A, R)} trCl (y, A, R))$
60	17 58 59	sylanbrc	$⊢ θ \to \neg (x \in pred (x, A, R) \lor x \in ⋃_{y \in pred (x, A, R)} trCl (y, A, R))$
61	4	simp2bi	$⊢ θ \to x \in A$
62	5	bnj1414	$⊢ (R FrSe A \land x \in A) \to trCl (x, A, R) = B$
63	9 61 62	syl2anc	$⊢ θ \to trCl (x, A, R) = B$
64	63	eleq2d	$⊢ θ \to (x \in trCl (x, A, R) \leftrightarrow x \in B)$
65	5	bnj1138	$⊢ x \in B \leftrightarrow (x \in pred (x, A, R) \lor x \in ⋃_{y \in pred (x, A, R)} trCl (y, A, R))$
66	64 65	syl6bb	$⊢ θ \to (x \in trCl (x, A, R) \leftrightarrow (x \in pred (x, A, R) \lor x \in ⋃_{y \in pred (x, A, R)} trCl (y, A, R)))$
67	60 66	mtbird	$⊢ θ \to \neg x \in trCl (x, A, R)$
68	67 2	sylibr	$⊢ θ \to ψ$
69	4 68	sylbir	$⊢ (φ \land x \in A \land χ) \to ψ$
70	69	3exp	$⊢ φ \to (x \in A \to (χ \to ψ))$
71	70	ralrimiv	$⊢ φ \to \forall x \in A (χ \to ψ)$
72	3	bnj1204	$⊢ (R FrSe A \land \forall x \in A (χ \to ψ)) \to \forall x \in A ψ$
73	6 71 72	syl2anc	$⊢ φ \to \forall x \in A ψ$
74	2	ralbii	$⊢ \forall x \in A ψ \leftrightarrow \forall x \in A \neg x \in trCl (x, A, R)$
75	73 74	sylib	$⊢ φ \to \forall x \in A \neg x \in trCl (x, A, R)$

Metamath Proof Explorer

Theorem bnj1417

Proof