Theorem snhesn

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

	Ref	Expression
Assertion	snhesn	⊢ { ⟨ 𝐴 , 𝐴 ⟩ } hereditary { 𝐵 }

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	elima3	⊢ ( 𝑥 ∈ ( { ⟨ 𝐴 , 𝐴 ⟩ } “ { 𝐵 } ) ↔ ∃ 𝑦 ( 𝑦 ∈ { 𝐵 } ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐴 ⟩ } ) )
3		velsn	⊢ ( 𝑥 ∈ { 𝐵 } ↔ 𝑥 = 𝐵 )
4	2 3	imbi12i	⊢ ( ( 𝑥 ∈ ( { ⟨ 𝐴 , 𝐴 ⟩ } “ { 𝐵 } ) → 𝑥 ∈ { 𝐵 } ) ↔ ( ∃ 𝑦 ( 𝑦 ∈ { 𝐵 } ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐴 ⟩ } ) → 𝑥 = 𝐵 ) )
5	4	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ ( { ⟨ 𝐴 , 𝐴 ⟩ } “ { 𝐵 } ) → 𝑥 ∈ { 𝐵 } ) ↔ ∀ 𝑥 ( ∃ 𝑦 ( 𝑦 ∈ { 𝐵 } ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐴 ⟩ } ) → 𝑥 = 𝐵 ) )
6		velsn	⊢ ( 𝑦 ∈ { 𝐵 } ↔ 𝑦 = 𝐵 )
7		opex	⊢ ⟨ 𝑦 , 𝑥 ⟩ ∈ V
8	7	elsn	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐴 ⟩ } ↔ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝐴 , 𝐴 ⟩ )
9		vex	⊢ 𝑦 ∈ V
10	9 1	opth	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝐴 , 𝐴 ⟩ ↔ ( 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) )
11	8 10	bitri	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐴 ⟩ } ↔ ( 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) )
12	6 11	anbi12i	⊢ ( ( 𝑦 ∈ { 𝐵 } ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐴 ⟩ } ) ↔ ( 𝑦 = 𝐵 ∧ ( 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) ) )
13		3anass	⊢ ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) ↔ ( 𝑦 = 𝐵 ∧ ( 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) ) )
14	12 13	bitr4i	⊢ ( ( 𝑦 ∈ { 𝐵 } ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐴 ⟩ } ) ↔ ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) )
15		simp3	⊢ ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐴 )
16		simp2	⊢ ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) → 𝑦 = 𝐴 )
17		simp1	⊢ ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) → 𝑦 = 𝐵 )
18	15 16 17	3eqtr2d	⊢ ( ( 𝑦 = 𝐵 ∧ 𝑦 = 𝐴 ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐵 )
19	14 18	sylbi	⊢ ( ( 𝑦 ∈ { 𝐵 } ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐴 ⟩ } ) → 𝑥 = 𝐵 )
20	19	exlimiv	⊢ ( ∃ 𝑦 ( 𝑦 ∈ { 𝐵 } ∧ ⟨ 𝑦 , 𝑥 ⟩ ∈ { ⟨ 𝐴 , 𝐴 ⟩ } ) → 𝑥 = 𝐵 )
21	5 20	mpgbir	⊢ ∀ 𝑥 ( 𝑥 ∈ ( { ⟨ 𝐴 , 𝐴 ⟩ } “ { 𝐵 } ) → 𝑥 ∈ { 𝐵 } )
22		df-ss	⊢ ( ( { ⟨ 𝐴 , 𝐴 ⟩ } “ { 𝐵 } ) ⊆ { 𝐵 } ↔ ∀ 𝑥 ( 𝑥 ∈ ( { ⟨ 𝐴 , 𝐴 ⟩ } “ { 𝐵 } ) → 𝑥 ∈ { 𝐵 } ) )
23	21 22	mpbir	⊢ ( { ⟨ 𝐴 , 𝐴 ⟩ } “ { 𝐵 } ) ⊆ { 𝐵 }
24		df-he	⊢ ( { ⟨ 𝐴 , 𝐴 ⟩ } hereditary { 𝐵 } ↔ ( { ⟨ 𝐴 , 𝐴 ⟩ } “ { 𝐵 } ) ⊆ { 𝐵 } )
25	23 24	mpbir	⊢ { ⟨ 𝐴 , 𝐴 ⟩ } hereditary { 𝐵 }