ssclem

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

		Ref	Expression
	Hypothesis	isssc.1	$⊢ φ \to H Fn (S \times S)$
	Assertion	ssclem	$⊢ φ \to (H \in V \leftrightarrow S \in V)$

Step	Hyp	Ref	Expression
1		isssc.1	$⊢ φ \to H Fn (S \times S)$
2		dmxpid	$⊢ dom (S \times S) = S$
3	1	fndmd	$⊢ φ \to dom H = S \times S$
4	3	adantr	$⊢ (φ \land H \in V) \to dom H = S \times S$
5		dmexg	$⊢ H \in V \to dom H \in V$
6	5	adantl	$⊢ (φ \land H \in V) \to dom H \in V$
7	4 6	eqeltrrd	$⊢ (φ \land H \in V) \to S \times S \in V$
8	7	dmexd	$⊢ (φ \land H \in V) \to dom (S \times S) \in V$
9	2 8	eqeltrrid	$⊢ (φ \land H \in V) \to S \in V$
10		sqxpexg	$⊢ S \in V \to S \times S \in V$
11		fnex	$⊢ (H Fn (S \times S) \land S \times S \in V) \to H \in V$
12	1 10 11	syl2an	$⊢ (φ \land S \in V) \to H \in V$
13	9 12	impbida	$⊢ φ \to (H \in V \leftrightarrow S \in V)$

Metamath Proof Explorer