Theorem bnj110

Description: Well-founded induction restricted to a set ( A e. _V ). The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj110.1	$$⊢A\in \mathrm{V}$$
	bnj110.2	$$⊢\psi \leftrightarrow \forall y\in A\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
Assertion	bnj110	$$⊢\left(R\mathrm{Fr}A\wedge \forall x\in A\left(\psi \to \phi \right)\right)\to \forall x\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		bnj110.1	$$⊢A\in \mathrm{V}$$
2		bnj110.2	$$⊢\psi \leftrightarrow \forall y\in A\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
3		ralnex	$$⊢\forall z\in \left\{x\in A|\neg \phi \right\}\neg \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \leftrightarrow \neg \exists z\in \left\{x\in A|\neg \phi \right\}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
4		sbcng	$$⊢z\in \mathrm{V}\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \neg \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
5	4	elv	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \phi \leftrightarrow \neg \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
6	5	bicomi	$$⊢\neg \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \phi$$
7	6	ralbii	$$⊢\forall z\in \left\{x\in A|\neg \phi \right\}\neg \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \leftrightarrow \forall z\in \left\{x\in A|\neg \phi \right\}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \phi$$
8	3 7	bitr3i	$$⊢\neg \exists z\in \left\{x\in A|\neg \phi \right\}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \leftrightarrow \forall z\in \left\{x\in A|\neg \phi \right\}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \phi$$
9		df-rab	$$⊢\left\{x\in A|\neg \phi \right\}=\left\{x|\left(x\in A\wedge \neg \phi \right)\right\}$$
10	9	eleq2i	$$⊢z\in \left\{x\in A|\neg \phi \right\}\leftrightarrow z\in \left\{x|\left(x\in A\wedge \neg \phi \right)\right\}$$
11		df-sbc	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(x\in A\wedge \neg \phi \right)\leftrightarrow z\in \left\{x|\left(x\in A\wedge \neg \phi \right)\right\}$$
12		sbcan	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(x\in A\wedge \neg \phi \right)\leftrightarrow \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}x\in A\wedge \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \phi \right)$$
13		sbcel1v	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}x\in A\leftrightarrow z\in A$$
14	13	anbi1i	$$⊢\left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}x\in A\wedge \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \phi \right)\leftrightarrow \left(z\in A\wedge \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \phi \right)$$
15	12 14	bitri	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(x\in A\wedge \neg \phi \right)\leftrightarrow \left(z\in A\wedge \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \phi \right)$$
16	11 15	bitr3i	$$⊢z\in \left\{x|\left(x\in A\wedge \neg \phi \right)\right\}\leftrightarrow \left(z\in A\wedge \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \phi \right)$$
17	10 16	bitri	$$⊢z\in \left\{x\in A|\neg \phi \right\}\leftrightarrow \left(z\in A\wedge \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \phi \right)$$
18	17	simprbi	$$⊢z\in \left\{x\in A|\neg \phi \right\}\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\neg \phi$$
19	8 18	mprgbir	$$⊢\neg \exists z\in \left\{x\in A|\neg \phi \right\}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
20	1	rabex	$$⊢\left\{x\in A|\neg \phi \right\}\in \mathrm{V}$$
21	20	biantrur	$$⊢R\mathrm{Fr}A\leftrightarrow \left(\left\{x\in A|\neg \phi \right\}\in \mathrm{V}\wedge R\mathrm{Fr}A\right)$$
22		rexnal	$$⊢\exists x\in A\neg \phi \leftrightarrow \neg \forall x\in A\phi$$
23		rabn0	$$⊢\left\{x\in A|\neg \phi \right\}\ne \varnothing \leftrightarrow \exists x\in A\neg \phi$$
24		ssrab2	$$⊢\left\{x\in A|\neg \phi \right\}\subseteq A$$
25	24	biantrur	$$⊢\left\{x\in A|\neg \phi \right\}\ne \varnothing \leftrightarrow \left(\left\{x\in A|\neg \phi \right\}\subseteq A\wedge \left\{x\in A|\neg \phi \right\}\ne \varnothing \right)$$
26	23 25	bitr3i	$$⊢\exists x\in A\neg \phi \leftrightarrow \left(\left\{x\in A|\neg \phi \right\}\subseteq A\wedge \left\{x\in A|\neg \phi \right\}\ne \varnothing \right)$$
27	22 26	bitr3i	$$⊢\neg \forall x\in A\phi \leftrightarrow \left(\left\{x\in A|\neg \phi \right\}\subseteq A\wedge \left\{x\in A|\neg \phi \right\}\ne \varnothing \right)$$
28		fri	$$⊢\left(\left(\left\{x\in A|\neg \phi \right\}\in \mathrm{V}\wedge R\mathrm{Fr}A\right)\wedge \left(\left\{x\in A|\neg \phi \right\}\subseteq A\wedge \left\{x\in A|\neg \phi \right\}\ne \varnothing \right)\right)\to \exists z\in \left\{x\in A|\neg \phi \right\}\forall w\in \left\{x\in A|\neg \phi \right\}\neg wRz$$
29	21 27 28	syl2anb	$$⊢\left(R\mathrm{Fr}A\wedge \neg \forall x\in A\phi \right)\to \exists z\in \left\{x\in A|\neg \phi \right\}\forall w\in \left\{x\in A|\neg \phi \right\}\neg wRz$$
30		eqid	$$⊢\left\{x\in A|\neg \phi \right\}=\left\{x\in A|\neg \phi \right\}$$
31	30	bnj23	$$⊢\forall w\in \left\{x\in A|\neg \phi \right\}\neg wRz\to \forall y\in A\left(yRz\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
32		df-ral	$$⊢\forall y\in A\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \forall y\left(y\in A\to \left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
33	32	sbcbii	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\forall y\in A\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\forall y\left(y\in A\to \left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
34		sbcal	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\forall y\left(y\in A\to \left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \forall y\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(y\in A\to \left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
35		sbcimg	$$⊢z\in \mathrm{V}\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(y\in A\to \left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}y\in A\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\right)$$
36	35	elv	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(y\in A\to \left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}y\in A\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
37		vex	$$⊢z\in \mathrm{V}$$
38		nfv	$$⊢Ⅎxy\in A$$
39	37 38	sbcgfi	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}y\in A\leftrightarrow y\in A$$
40		sbcimg	$$⊢z\in \mathrm{V}\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}yRx\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
41	40	elv	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}yRx\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
42		sbcbr2g	$$⊢z\in \mathrm{V}\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}yRx\leftrightarrow yR⦋z/x⦌x\right)$$
43	42	elv	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}yRx\leftrightarrow yR⦋z/x⦌x$$
44	37	csbvargi	$$⊢⦋z/x⦌x=z$$
45	44	breq2i	$$⊢yR⦋z/x⦌x\leftrightarrow yRz$$
46	43 45	bitri	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}yRx\leftrightarrow yRz$$
47		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
48	37 47	sbcgfi	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
49	46 48	imbi12i	$$⊢\left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}yRx\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(yRz\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
50	41 49	bitri	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(yRz\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
51	39 50	imbi12i	$$⊢\left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}y\in A\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(y\in A\to \left(yRz\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
52	36 51	bitri	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(y\in A\to \left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(y\in A\to \left(yRz\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
53	52	albii	$$⊢\forall y\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\left(y\in A\to \left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \forall y\left(y\in A\to \left(yRz\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
54	34 53	bitri	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\forall y\left(y\in A\to \left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \forall y\left(y\in A\to \left(yRz\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
55	33 54	bitri	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\forall y\in A\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \forall y\left(y\in A\to \left(yRz\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
56	2	sbcbii	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\forall y\in A\left(yRx\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
57		df-ral	$$⊢\forall y\in A\left(yRz\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \forall y\left(y\in A\to \left(yRz\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
58	55 56 57	3bitr4i	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \leftrightarrow \forall y\in A\left(yRz\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
59	31 58	sylibr	$$⊢\forall w\in \left\{x\in A|\neg \phi \right\}\neg wRz\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi$$
60	29 59	bnj31	$$⊢\left(R\mathrm{Fr}A\wedge \neg \forall x\in A\phi \right)\to \exists z\in \left\{x\in A|\neg \phi \right\}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi$$
61		nfv	$$⊢Ⅎz\left(\psi \to \phi \right)$$
62		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi$$
63		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
64	62 63	nfim	$$⊢Ⅎx\left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
65		sbceq1a	$$⊢x=z\to \left(\psi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \right)$$
66		sbceq1a	$$⊢x=z\to \left(\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
67	65 66	imbi12d	$$⊢x=z\to \left(\left(\psi \to \phi \right)\leftrightarrow \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)\right)$$
68	61 64 67	cbvralw	$$⊢\forall x\in A\left(\psi \to \phi \right)\leftrightarrow \forall z\in A\left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
69		elrabi	$$⊢z\in \left\{x\in A|\neg \phi \right\}\to z\in A$$
70	69	imim1i	$$⊢\left(z\in A\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)\right)\to \left(z\in \left\{x\in A|\neg \phi \right\}\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)\right)$$
71	70	ralimi2	$$⊢\forall z\in A\left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)\to \forall z\in \left\{x\in A|\neg \phi \right\}\left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
72	68 71	sylbi	$$⊢\forall x\in A\left(\psi \to \phi \right)\to \forall z\in \left\{x\in A|\neg \phi \right\}\left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
73		rexim	$$⊢\forall z\in \left\{x\in A|\neg \phi \right\}\left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)\to \left(\exists z\in \left\{x\in A|\neg \phi \right\}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \to \exists z\in \left\{x\in A|\neg \phi \right\}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
74	72 73	syl	$$⊢\forall x\in A\left(\psi \to \phi \right)\to \left(\exists z\in \left\{x\in A|\neg \phi \right\}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\psi \to \exists z\in \left\{x\in A|\neg \phi \right\}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
75	60 74	mpan9	$$⊢\left(\left(R\mathrm{Fr}A\wedge \neg \forall x\in A\phi \right)\wedge \forall x\in A\left(\psi \to \phi \right)\right)\to \exists z\in \left\{x\in A|\neg \phi \right\}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
76	75	an32s	$$⊢\left(\left(R\mathrm{Fr}A\wedge \forall x\in A\left(\psi \to \phi \right)\right)\wedge \neg \forall x\in A\phi \right)\to \exists z\in \left\{x\in A|\neg \phi \right\}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
77	19 76	mto	$$⊢\neg \left(\left(R\mathrm{Fr}A\wedge \forall x\in A\left(\psi \to \phi \right)\right)\wedge \neg \forall x\in A\phi \right)$$
78		iman	$$⊢\left(\left(R\mathrm{Fr}A\wedge \forall x\in A\left(\psi \to \phi \right)\right)\to \forall x\in A\phi \right)\leftrightarrow \neg \left(\left(R\mathrm{Fr}A\wedge \forall x\in A\left(\psi \to \phi \right)\right)\wedge \neg \forall x\in A\phi \right)$$
79	77 78	mpbir	$$⊢\left(R\mathrm{Fr}A\wedge \forall x\in A\left(\psi \to \phi \right)\right)\to \forall x\in A\phi$$