Metamath Proof Explorer

Theorem snhesn

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

Ref Expression
Assertion snhesn 
|- { <. A , A >. } hereditary { B }

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 elima3 
 |-  ( x e. ( { <. A , A >. } " { B } ) <-> E. y ( y e. { B } /\ <. y , x >. e. { <. A , A >. } ) )
3 velsn 
 |-  ( x e. { B } <-> x = B )
4 2 3 imbi12i 
 |-  ( ( x e. ( { <. A , A >. } " { B } ) -> x e. { B } ) <-> ( E. y ( y e. { B } /\ <. y , x >. e. { <. A , A >. } ) -> x = B ) )
5 4 albii 
 |-  ( A. x ( x e. ( { <. A , A >. } " { B } ) -> x e. { B } ) <-> A. x ( E. y ( y e. { B } /\ <. y , x >. e. { <. A , A >. } ) -> x = B ) )
6 velsn 
 |-  ( y e. { B } <-> y = B )
7 opex 
 |-  <. y , x >. e. _V
8 7 elsn 
 |-  ( <. y , x >. e. { <. A , A >. } <-> <. y , x >. = <. A , A >. )
9 vex 
 |-  y e. _V
10 9 1 opth 
 |-  ( <. y , x >. = <. A , A >. <-> ( y = A /\ x = A ) )
11 8 10 bitri 
 |-  ( <. y , x >. e. { <. A , A >. } <-> ( y = A /\ x = A ) )
12 6 11 anbi12i 
 |-  ( ( y e. { B } /\ <. y , x >. e. { <. A , A >. } ) <-> ( y = B /\ ( y = A /\ x = A ) ) )
13 3anass 
 |-  ( ( y = B /\ y = A /\ x = A ) <-> ( y = B /\ ( y = A /\ x = A ) ) )
14 12 13 bitr4i 
 |-  ( ( y e. { B } /\ <. y , x >. e. { <. A , A >. } ) <-> ( y = B /\ y = A /\ x = A ) )
15 simp3 
 |-  ( ( y = B /\ y = A /\ x = A ) -> x = A )
16 simp2 
 |-  ( ( y = B /\ y = A /\ x = A ) -> y = A )
17 simp1 
 |-  ( ( y = B /\ y = A /\ x = A ) -> y = B )
18 15 16 17 3eqtr2d 
 |-  ( ( y = B /\ y = A /\ x = A ) -> x = B )
19 14 18 sylbi 
 |-  ( ( y e. { B } /\ <. y , x >. e. { <. A , A >. } ) -> x = B )
20 19 exlimiv 
 |-  ( E. y ( y e. { B } /\ <. y , x >. e. { <. A , A >. } ) -> x = B )
21 5 20 mpgbir 
 |-  A. x ( x e. ( { <. A , A >. } " { B } ) -> x e. { B } )
22 dfss2 
 |-  ( ( { <. A , A >. } " { B } ) C_ { B } <-> A. x ( x e. ( { <. A , A >. } " { B } ) -> x e. { B } ) )
23 21 22 mpbir 
 |-  ( { <. A , A >. } " { B } ) C_ { B }
24 df-he 
 |-  ( { <. A , A >. } hereditary { B } <-> ( { <. A , A >. } " { B } ) C_ { B } )
25 23 24 mpbir 
 |-  { <. A , A >. } hereditary { B }