bnj1204

		Ref	Expression
	Hypothesis	bnj1204.1	$⊢ ψ \leftrightarrow \forall y \in A (y R x \to \underset{˙}{[} y / x \underset{˙}{]} φ)$
	Assertion	bnj1204	$⊢ (R FrSe A \land \forall x \in A (ψ \to φ)) \to \forall x \in A φ$

Proof

Step	Hyp	Ref	Expression
1		bnj1204.1	$⊢ ψ \leftrightarrow \forall y \in A (y R x \to \underset{˙}{[} y / x \underset{˙}{]} φ)$
2		simp1	$⊢ (R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \to R FrSe A$
3		ssrab2	$⊢ \{x \in A \| \neg φ\} \subseteq A$
4	3	a1i	$⊢ (R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \to \{x \in A \| \neg φ\} \subseteq A$
5		simp3	$⊢ (R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \to \exists x \in A \neg φ$
6		rabn0	$⊢ \{x \in A \| \neg φ\} \neq \emptyset \leftrightarrow \exists x \in A \neg φ$
7	5 6	sylibr	$⊢ (R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \to \{x \in A \| \neg φ\} \neq \emptyset$
8		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| \neg φ\}$
9	8	nfcrii	$⊢ z \in \{x \in A \| \neg φ\} \to \forall x z \in \{x \in A \| \neg φ\}$
10	9	bnj1228	$⊢ (R FrSe A \land \{x \in A \| \neg φ\} \subseteq A \land \{x \in A \| \neg φ\} \neq \emptyset) \to \exists x \in \{x \in A \| \neg φ\} \forall y \in \{x \in A \| \neg φ\} \neg y R x$
11	2 4 7 10	syl3anc	$⊢ (R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \to \exists x \in \{x \in A \| \neg φ\} \forall y \in \{x \in A \| \neg φ\} \neg y R x$
12		biid	$⊢ ((R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \land x \in \{x \in A \| \neg φ\} \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \leftrightarrow ((R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \land x \in \{x \in A \| \neg φ\} \land \forall y \in \{x \in A \| \neg φ\} \neg y R x)$
13		nfv	$⊢ Ⅎ x R FrSe A$
14		nfra1	$⊢ Ⅎ x \forall x \in A (ψ \to φ)$
15		nfre1	$⊢ Ⅎ x \exists x \in A \neg φ$
16	13 14 15	nf3an	$⊢ Ⅎ x (R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ)$
17	16	nf5ri	$⊢ (R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \to \forall x (R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ)$
18	11 12 17	bnj1521	$⊢ (R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \to \exists x ((R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \land x \in \{x \in A \| \neg φ\} \land \forall y \in \{x \in A \| \neg φ\} \neg y R x)$
19		eqid	$⊢ \{x \in A \| \neg φ\} = \{x \in A \| \neg φ\}$
20	19 12	bnj1212	$⊢ ((R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \land x \in \{x \in A \| \neg φ\} \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to x \in A$
21		nfra1	$⊢ Ⅎ y \forall y \in \{x \in A \| \neg φ\} \neg y R x$
22		simp3	$⊢ (y \in A \land y R x \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to \forall y \in \{x \in A \| \neg φ\} \neg y R x$
23	22	bnj1211	$⊢ (y \in A \land y R x \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to \forall y (y \in \{x \in A \| \neg φ\} \to \neg y R x)$
24		con2b	$⊢ (y \in \{x \in A \| \neg φ\} \to \neg y R x) \leftrightarrow (y R x \to \neg y \in \{x \in A \| \neg φ\})$
25	24	albii	$⊢ \forall y (y \in \{x \in A \| \neg φ\} \to \neg y R x) \leftrightarrow \forall y (y R x \to \neg y \in \{x \in A \| \neg φ\})$
26	23 25	sylib	$⊢ (y \in A \land y R x \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to \forall y (y R x \to \neg y \in \{x \in A \| \neg φ\})$
27		simp2	$⊢ (y \in A \land y R x \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to y R x$
28		sp	$⊢ \forall y (y R x \to \neg y \in \{x \in A \| \neg φ\}) \to (y R x \to \neg y \in \{x \in A \| \neg φ\})$
29	26 27 28	sylc	$⊢ (y \in A \land y R x \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to \neg y \in \{x \in A \| \neg φ\}$
30		simp1	$⊢ (y \in A \land y R x \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to y \in A$
31		nfcv	$⊢ \underline{Ⅎ} x A$
32	31	elrabsf	$⊢ y \in \{x \in A \| \neg φ\} \leftrightarrow (y \in A \land \underset{˙}{[} y / x \underset{˙}{]} \neg φ)$
33		vex	$⊢ y \in V$
34		sbcng	$⊢ y \in V \to (\underset{˙}{[} y / x \underset{˙}{]} \neg φ \leftrightarrow \neg \underset{˙}{[} y / x \underset{˙}{]} φ)$
35	33 34	ax-mp	$⊢ \underset{˙}{[} y / x \underset{˙}{]} \neg φ \leftrightarrow \neg \underset{˙}{[} y / x \underset{˙}{]} φ$
36	35	anbi2i	$⊢ (y \in A \land \underset{˙}{[} y / x \underset{˙}{]} \neg φ) \leftrightarrow (y \in A \land \neg \underset{˙}{[} y / x \underset{˙}{]} φ)$
37	32 36	bitri	$⊢ y \in \{x \in A \| \neg φ\} \leftrightarrow (y \in A \land \neg \underset{˙}{[} y / x \underset{˙}{]} φ)$
38	37	notbii	$⊢ \neg y \in \{x \in A \| \neg φ\} \leftrightarrow \neg (y \in A \land \neg \underset{˙}{[} y / x \underset{˙}{]} φ)$
39		imnan	$⊢ (y \in A \to \neg \neg \underset{˙}{[} y / x \underset{˙}{]} φ) \leftrightarrow \neg (y \in A \land \neg \underset{˙}{[} y / x \underset{˙}{]} φ)$
40	38 39	sylbb2	$⊢ \neg y \in \{x \in A \| \neg φ\} \to (y \in A \to \neg \neg \underset{˙}{[} y / x \underset{˙}{]} φ)$
41	40	imp	$⊢ (\neg y \in \{x \in A \| \neg φ\} \land y \in A) \to \neg \neg \underset{˙}{[} y / x \underset{˙}{]} φ$
42	41	notnotrd	$⊢ (\neg y \in \{x \in A \| \neg φ\} \land y \in A) \to \underset{˙}{[} y / x \underset{˙}{]} φ$
43	29 30 42	syl2anc	$⊢ (y \in A \land y R x \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to \underset{˙}{[} y / x \underset{˙}{]} φ$
44	43	3expa	$⊢ ((y \in A \land y R x) \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to \underset{˙}{[} y / x \underset{˙}{]} φ$
45	44	expcom	$⊢ \forall y \in \{x \in A \| \neg φ\} \neg y R x \to ((y \in A \land y R x) \to \underset{˙}{[} y / x \underset{˙}{]} φ)$
46	45	expd	$⊢ \forall y \in \{x \in A \| \neg φ\} \neg y R x \to (y \in A \to (y R x \to \underset{˙}{[} y / x \underset{˙}{]} φ))$
47	21 46	ralrimi	$⊢ \forall y \in \{x \in A \| \neg φ\} \neg y R x \to \forall y \in A (y R x \to \underset{˙}{[} y / x \underset{˙}{]} φ)$
48	47 1	sylibr	$⊢ \forall y \in \{x \in A \| \neg φ\} \neg y R x \to ψ$
49	48	3ad2ant3	$⊢ ((R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \land x \in \{x \in A \| \neg φ\} \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to ψ$
50		simp12	$⊢ ((R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \land x \in \{x \in A \| \neg φ\} \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to \forall x \in A (ψ \to φ)$
51		simp3	$⊢ (x \in A \land ψ \land \forall x \in A (ψ \to φ)) \to \forall x \in A (ψ \to φ)$
52	51	bnj1211	$⊢ (x \in A \land ψ \land \forall x \in A (ψ \to φ)) \to \forall x (x \in A \to (ψ \to φ))$
53		simp1	$⊢ (x \in A \land ψ \land \forall x \in A (ψ \to φ)) \to x \in A$
54		simp2	$⊢ (x \in A \land ψ \land \forall x \in A (ψ \to φ)) \to ψ$
55		sp	$⊢ \forall x (x \in A \to (ψ \to φ)) \to (x \in A \to (ψ \to φ))$
56	52 53 54 55	syl3c	$⊢ (x \in A \land ψ \land \forall x \in A (ψ \to φ)) \to φ$
57	20 49 50 56	syl3anc	$⊢ ((R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \land x \in \{x \in A \| \neg φ\} \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to φ$
58		rabid	$⊢ x \in \{x \in A \| \neg φ\} \leftrightarrow (x \in A \land \neg φ)$
59	58	simprbi	$⊢ x \in \{x \in A \| \neg φ\} \to \neg φ$
60	59	3ad2ant2	$⊢ ((R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ) \land x \in \{x \in A \| \neg φ\} \land \forall y \in \{x \in A \| \neg φ\} \neg y R x) \to \neg φ$
61	18 57 60	bnj1304	$⊢ \neg (R FrSe A \land \forall x \in A (ψ \to φ) \land \exists x \in A \neg φ)$
62	61	bnj1224	$⊢ (R FrSe A \land \forall x \in A (ψ \to φ)) \to \neg \exists x \in A \neg φ$
63		dfral2	$⊢ \forall x \in A φ \leftrightarrow \neg \exists x \in A \neg φ$
64	62 63	sylibr	$⊢ (R FrSe A \land \forall x \in A (ψ \to φ)) \to \forall x \in A φ$

Metamath Proof Explorer

Theorem bnj1204

Proof