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