Theorem sbiota1

Description: Theorem *14.25 in WhiteheadRussell p. 192. (Contributed by Andrew Salmon, 12-Jul-2011)

	Ref	Expression
Assertion	sbiota1	$$⊢\exists !x\phi \to \left(\forall x\left(\phi \to \psi \right)\leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		eu6	$$⊢\exists !x\phi \leftrightarrow \exists y\forall x\left(\phi \leftrightarrow x=y\right)$$
2	1	biimpi	$$⊢\exists !x\phi \to \exists y\forall x\left(\phi \leftrightarrow x=y\right)$$
3		iota4	$$⊢\exists !x\phi \to \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi$$
4		iotaval	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\iota x|\phi \right)=y$$
5	4	eqcomd	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to y=\left(\iota x|\phi \right)$$
6		spsbim	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\left[y/x\right]\phi \to \left[y/x\right]\psi \right)$$
7		sbsbc	$$⊢\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
8		sbsbc	$$⊢\left[y/x\right]\psi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi$$
9	6 7 8	3imtr3g	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)$$
10		dfsbcq	$$⊢y=\left(\iota x|\phi \right)\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi \right)$$
11		dfsbcq	$$⊢y=\left(\iota x|\phi \right)\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)$$
12	10 11	imbi12d	$$⊢y=\left(\iota x|\phi \right)\to \left(\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)\right)$$
13	9 12	syl5ib	$$⊢y=\left(\iota x|\phi \right)\to \left(\forall x\left(\phi \to \psi \right)\to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)\right)$$
14	13	com23	$$⊢y=\left(\iota x|\phi \right)\to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi \to \left(\forall x\left(\phi \to \psi \right)\to \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)\right)$$
15	5 14	syl	$$⊢\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi \to \left(\forall x\left(\phi \to \psi \right)\to \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)\right)$$
16	15	exlimiv	$$⊢\exists y\forall x\left(\phi \leftrightarrow x=y\right)\to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi \to \left(\forall x\left(\phi \to \psi \right)\to \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)\right)$$
17	2 3 16	sylc	$$⊢\exists !x\phi \to \left(\forall x\left(\phi \to \psi \right)\to \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)$$
18		iotaexeu	$$⊢\exists !x\phi \to \left(\iota x|\phi \right)\in \mathrm{V}$$
19	10 11	anbi12d	$$⊢y=\left(\iota x|\phi \right)\to \left(\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)\right)$$
20	19	imbi1d	$$⊢y=\left(\iota x|\phi \right)\to \left(\left(\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\to \exists x\left(\phi \wedge \psi \right)\right)\leftrightarrow \left(\left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)\to \exists x\left(\phi \wedge \psi \right)\right)\right)$$
21		sbcan	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\phi \wedge \psi \right)\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)$$
22		spesbc	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\phi \wedge \psi \right)\to \exists x\left(\phi \wedge \psi \right)$$
23	21 22	sylbir	$$⊢\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\psi \right)\to \exists x\left(\phi \wedge \psi \right)$$
24	20 23	vtoclg	$$⊢\left(\iota x|\phi \right)\in \mathrm{V}\to \left(\left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)\to \exists x\left(\phi \wedge \psi \right)\right)$$
25	24	expd	$$⊢\left(\iota x|\phi \right)\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\phi \to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \to \exists x\left(\phi \wedge \psi \right)\right)\right)$$
26	18 3 25	sylc	$$⊢\exists !x\phi \to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \to \exists x\left(\phi \wedge \psi \right)\right)$$
27	26	anc2li	$$⊢\exists !x\phi \to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \to \left(\exists !x\phi \wedge \exists x\left(\phi \wedge \psi \right)\right)\right)$$
28		eupicka	$$⊢\left(\exists !x\phi \wedge \exists x\left(\phi \wedge \psi \right)\right)\to \forall x\left(\phi \to \psi \right)$$
29	27 28	syl6	$$⊢\exists !x\phi \to \left(\underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \to \forall x\left(\phi \to \psi \right)\right)$$
30	17 29	impbid	$$⊢\exists !x\phi \to \left(\forall x\left(\phi \to \psi \right)\leftrightarrow \underset{\dot{}}{[}\left(\iota x|\phi \right)/x\underset{\dot{}}{]}\psi \right)$$