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