Metamath Proof Explorer


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 dfss2 ( ( { ⟨ 𝐴 , 𝐴 ⟩ } “ { 𝐵 } ) ⊆ { 𝐵 } ↔ ∀ 𝑥 ( 𝑥 ∈ ( { ⟨ 𝐴 , 𝐴 ⟩ } “ { 𝐵 } ) → 𝑥 ∈ { 𝐵 } ) )
23 21 22 mpbir ( { ⟨ 𝐴 , 𝐴 ⟩ } “ { 𝐵 } ) ⊆ { 𝐵 }
24 df-he ( { ⟨ 𝐴 , 𝐴 ⟩ } hereditary { 𝐵 } ↔ ( { ⟨ 𝐴 , 𝐴 ⟩ } “ { 𝐵 } ) ⊆ { 𝐵 } )
25 23 24 mpbir { ⟨ 𝐴 , 𝐴 ⟩ } hereditary { 𝐵 }