ssclem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ssclem		Structured version Visualization version GIF version

Theorem ssclem 16460

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

**Hypothesis**
Ref	Expression
isssc.1	⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))

**Assertion**
Ref	Expression
ssclem	⊢ (𝜑 → (𝐻 ∈ V ↔ 𝑆 ∈ V))

**Proof of Theorem ssclem**
Step	Hyp	Ref	Expression
1		dmxpid 5334	. . 3 ⊢ dom (𝑆 × 𝑆) = 𝑆
2		isssc.1	. . . . . . 7 ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))
3		fndm 5978	. . . . . . 7 ⊢ (𝐻 Fn (𝑆 × 𝑆) → dom 𝐻 = (𝑆 × 𝑆))
4	2, 3	syl 17	. . . . . 6 ⊢ (𝜑 → dom 𝐻 = (𝑆 × 𝑆))
5	4	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐻 ∈ V) → dom 𝐻 = (𝑆 × 𝑆))
6		dmexg 7082	. . . . . 6 ⊢ (𝐻 ∈ V → dom 𝐻 ∈ V)
7	6	adantl 482	. . . . 5 ⊢ ((𝜑 ∧ 𝐻 ∈ V) → dom 𝐻 ∈ V)
8	5, 7	eqeltrrd 2700	. . . 4 ⊢ ((𝜑 ∧ 𝐻 ∈ V) → (𝑆 × 𝑆) ∈ V)
9		dmexg 7082	. . . 4 ⊢ ((𝑆 × 𝑆) ∈ V → dom (𝑆 × 𝑆) ∈ V)
10	8, 9	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝐻 ∈ V) → dom (𝑆 × 𝑆) ∈ V)
11	1, 10	syl5eqelr 2704	. 2 ⊢ ((𝜑 ∧ 𝐻 ∈ V) → 𝑆 ∈ V)
12		sqxpexg 6948	. . 3 ⊢ (𝑆 ∈ V → (𝑆 × 𝑆) ∈ V)
13		fnex 6466	. . 3 ⊢ ((𝐻 Fn (𝑆 × 𝑆) ∧ (𝑆 × 𝑆) ∈ V) → 𝐻 ∈ V)
14	2, 12, 13	syl2an 494	. 2 ⊢ ((𝜑 ∧ 𝑆 ∈ V) → 𝐻 ∈ V)
15	11, 14	impbida 876	1 ⊢ (𝜑 → (𝐻 ∈ V ↔ 𝑆 ∈ V))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1481 ∈ wcel 1988 Vcvv 3195 × cxp 5102 dom cdm 5104 Fn wfn 5871

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1720 ax-4 1735 ax-5 1837 ax-6 1886 ax-7 1933 ax-8 1990 ax-9 1997 ax-10 2017 ax-11 2032 ax-12 2045 ax-13 2244 ax-ext 2600 ax-rep 4762 ax-sep 4772 ax-nul 4780 ax-pow 4834 ax-pr 4897 ax-un 6934

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1038 df-tru 1484 df-ex 1703 df-nf 1708 df-sb 1879 df-eu 2472 df-mo 2473 df-clab 2607 df-cleq 2613 df-clel 2616 df-nfc 2751 df-ne 2792 df-ral 2914 df-rex 2915 df-reu 2916 df-rab 2918 df-v 3197 df-sbc 3430 df-csb 3527 df-dif 3570 df-un 3572 df-in 3574 df-ss 3581 df-nul 3908 df-if 4078 df-pw 4151 df-sn 4169 df-pr 4171 df-op 4175 df-uni 4428 df-iun 4513 df-br 4645 df-opab 4704 df-mpt 4721 df-id 5014 df-xp 5110 df-rel 5111 df-cnv 5112 df-co 5113 df-dm 5114 df-rn 5115 df-res 5116 df-ima 5117 df-iota 5839 df-fun 5878 df-fn 5879 df-f 5880 df-f1 5881 df-fo 5882 df-f1o 5883 df-fv 5884

This theorem is referenced by: ssc1 16462