Database
BASIC CATEGORY THEORY
Categories
Subcategories
ssclem
Next ⟩
isssc
Metamath Proof Explorer
Ascii
Unicode
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