This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssclem

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

Ref Expression
Hypothesis isssc.1 ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
Assertion ssclem ( 𝜑 → ( 𝐻 ∈ V ↔ 𝑆 ∈ V ) )

Proof

Step Hyp Ref Expression
1 isssc.1 ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
2 dmxpid ⊢ dom ( 𝑆 × 𝑆 ) = 𝑆
3 1 fndmd ⊢ ( 𝜑 → dom 𝐻 = ( 𝑆 × 𝑆 ) )
4 3 adantr ⊢ ( ( 𝜑 ∧ 𝐻 ∈ V ) → dom 𝐻 = ( 𝑆 × 𝑆 ) )
5 dmexg ⊢ ( 𝐻 ∈ V → dom 𝐻 ∈ V )
6 5 adantl ⊢ ( ( 𝜑 ∧ 𝐻 ∈ V ) → dom 𝐻 ∈ V )
7 4 6 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝐻 ∈ V ) → ( 𝑆 × 𝑆 ) ∈ V )
8 7 dmexd ⊢ ( ( 𝜑 ∧ 𝐻 ∈ V ) → dom ( 𝑆 × 𝑆 ) ∈ V )
9 2 8 eqeltrrid ⊢ ( ( 𝜑 ∧ 𝐻 ∈ V ) → 𝑆 ∈ V )
10 sqxpexg ⊢ ( 𝑆 ∈ V → ( 𝑆 × 𝑆 ) ∈ V )
11 fnex ⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝑆 × 𝑆 ) ∈ V ) → 𝐻 ∈ V )
12 1 10 11 syl2an ⊢ ( ( 𝜑 ∧ 𝑆 ∈ V ) → 𝐻 ∈ V )
13 9 12 impbida ⊢ ( 𝜑 → ( 𝐻 ∈ V ↔ 𝑆 ∈ V ) )