This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssclem

Description: Lemma for ssc1 and similar theorems. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypothesis isssc.1 
|- ( ph -> H Fn ( S X. S ) )
Assertion ssclem 
|- ( ph -> ( H e. _V <-> S e. _V ) )

Proof

Step Hyp Ref Expression
1 isssc.1 
 |-  ( ph -> H Fn ( S X. S ) )
2 dmxpid 
 |-  dom ( S X. S ) = S
3 1 fndmd 
 |-  ( ph -> dom H = ( S X. S ) )
4 3 adantr 
 |-  ( ( ph /\ H e. _V ) -> dom H = ( S X. S ) )
5 dmexg 
 |-  ( H e. _V -> dom H e. _V )
6 5 adantl 
 |-  ( ( ph /\ H e. _V ) -> dom H e. _V )
7 4 6 eqeltrrd 
 |-  ( ( ph /\ H e. _V ) -> ( S X. S ) e. _V )
8 7 dmexd 
 |-  ( ( ph /\ H e. _V ) -> dom ( S X. S ) e. _V )
9 2 8 eqeltrrid 
 |-  ( ( ph /\ H e. _V ) -> S e. _V )
10 sqxpexg 
 |-  ( S e. _V -> ( S X. S ) e. _V )
11 fnex 
 |-  ( ( H Fn ( S X. S ) /\ ( S X. S ) e. _V ) -> H e. _V )
12 1 10 11 syl2an 
 |-  ( ( ph /\ S e. _V ) -> H e. _V )
13 9 12 impbida 
 |-  ( ph -> ( H e. _V <-> S e. _V ) )