Metamath Proof Explorer


Theorem ssclem

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

Ref Expression
Hypothesis isssc.1 φ H Fn S × S
Assertion ssclem φ H V S V

Proof

Step Hyp Ref Expression
1 isssc.1 φ H Fn S × S
2 dmxpid dom S × S = S
3 1 fndmd φ dom H = S × S
4 3 adantr φ H V dom H = S × S
5 dmexg H V dom H V
6 5 adantl φ H V dom H V
7 4 6 eqeltrrd φ H V S × S V
8 7 dmexd φ H V dom S × S V
9 2 8 eqeltrrid φ H V S V
10 sqxpexg S V S × S V
11 fnex H Fn S × S S × S V H V
12 1 10 11 syl2an φ S V H V
13 9 12 impbida φ H V S V