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 ) )