Metamath Proof Explorer


Theorem ssclem

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

Ref Expression
Hypothesis isssc.1 φHFnS×S
Assertion ssclem φHVSV

Proof

Step Hyp Ref Expression
1 isssc.1 φHFnS×S
2 dmxpid domS×S=S
3 1 fndmd φdomH=S×S
4 3 adantr φHVdomH=S×S
5 dmexg HVdomHV
6 5 adantl φHVdomHV
7 4 6 eqeltrrd φHVS×SV
8 7 dmexd φHVdomS×SV
9 2 8 eqeltrrid φHVSV
10 sqxpexg SVS×SV
11 fnex HFnS×SS×SVHV
12 1 10 11 syl2an φSVHV
13 9 12 impbida φHVSV