Theorem snhesn

Description: Any singleton is hereditary in any singleton. (Contributed by RP, 28-Mar-2020)

	Ref	Expression
Assertion	snhesn	$$⊢\left\{⟨A,A⟩\right\}hereditary\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	elima3	$$⊢x\in \left\{⟨A,A⟩\right\}\left[\left\{B\right\}\right]\leftrightarrow \exists y\left(y\in \left\{B\right\}\wedge ⟨y,x⟩\in \left\{⟨A,A⟩\right\}\right)$$
3		velsn	$$⊢x\in \left\{B\right\}\leftrightarrow x=B$$
4	2 3	imbi12i	$$⊢\left(x\in \left\{⟨A,A⟩\right\}\left[\left\{B\right\}\right]\to x\in \left\{B\right\}\right)\leftrightarrow \left(\exists y\left(y\in \left\{B\right\}\wedge ⟨y,x⟩\in \left\{⟨A,A⟩\right\}\right)\to x=B\right)$$
5	4	albii	$$⊢\forall x\left(x\in \left\{⟨A,A⟩\right\}\left[\left\{B\right\}\right]\to x\in \left\{B\right\}\right)\leftrightarrow \forall x\left(\exists y\left(y\in \left\{B\right\}\wedge ⟨y,x⟩\in \left\{⟨A,A⟩\right\}\right)\to x=B\right)$$
6		velsn	$$⊢y\in \left\{B\right\}\leftrightarrow y=B$$
7		opex	$$⊢⟨y,x⟩\in \mathrm{V}$$
8	7	elsn	$$⊢⟨y,x⟩\in \left\{⟨A,A⟩\right\}\leftrightarrow ⟨y,x⟩=⟨A,A⟩$$
9		vex	$$⊢y\in \mathrm{V}$$
10	9 1	opth	$$⊢⟨y,x⟩=⟨A,A⟩\leftrightarrow \left(y=A\wedge x=A\right)$$
11	8 10	bitri	$$⊢⟨y,x⟩\in \left\{⟨A,A⟩\right\}\leftrightarrow \left(y=A\wedge x=A\right)$$
12	6 11	anbi12i	$$⊢\left(y\in \left\{B\right\}\wedge ⟨y,x⟩\in \left\{⟨A,A⟩\right\}\right)\leftrightarrow \left(y=B\wedge \left(y=A\wedge x=A\right)\right)$$
13		3anass	$$⊢\left(y=B\wedge y=A\wedge x=A\right)\leftrightarrow \left(y=B\wedge \left(y=A\wedge x=A\right)\right)$$
14	12 13	bitr4i	$$⊢\left(y\in \left\{B\right\}\wedge ⟨y,x⟩\in \left\{⟨A,A⟩\right\}\right)\leftrightarrow \left(y=B\wedge y=A\wedge x=A\right)$$
15		simp3	$$⊢\left(y=B\wedge y=A\wedge x=A\right)\to x=A$$
16		simp2	$$⊢\left(y=B\wedge y=A\wedge x=A\right)\to y=A$$
17		simp1	$$⊢\left(y=B\wedge y=A\wedge x=A\right)\to y=B$$
18	15 16 17	3eqtr2d	$$⊢\left(y=B\wedge y=A\wedge x=A\right)\to x=B$$
19	14 18	sylbi	$$⊢\left(y\in \left\{B\right\}\wedge ⟨y,x⟩\in \left\{⟨A,A⟩\right\}\right)\to x=B$$
20	19	exlimiv	$$⊢\exists y\left(y\in \left\{B\right\}\wedge ⟨y,x⟩\in \left\{⟨A,A⟩\right\}\right)\to x=B$$
21	5 20	mpgbir	$$⊢\forall x\left(x\in \left\{⟨A,A⟩\right\}\left[\left\{B\right\}\right]\to x\in \left\{B\right\}\right)$$
22		df-ss	$$⊢\left\{⟨A,A⟩\right\}\left[\left\{B\right\}\right]\subseteq \left\{B\right\}\leftrightarrow \forall x\left(x\in \left\{⟨A,A⟩\right\}\left[\left\{B\right\}\right]\to x\in \left\{B\right\}\right)$$
23	21 22	mpbir	$$⊢\left\{⟨A,A⟩\right\}\left[\left\{B\right\}\right]\subseteq \left\{B\right\}$$
24		df-he	$$⊢\left\{⟨A,A⟩\right\}hereditary\left\{B\right\}\leftrightarrow \left\{⟨A,A⟩\right\}\left[\left\{B\right\}\right]\subseteq \left\{B\right\}$$
25	23 24	mpbir	$$⊢\left\{⟨A,A⟩\right\}hereditary\left\{B\right\}$$