eldm3

Description: Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017)

		Ref	Expression
	Assertion	eldm3	$⊢ A \in dom B \leftrightarrow {B ↾}_{\{A\}} \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in dom B \to A \in V$
2		snprc	$⊢ \neg A \in V \leftrightarrow \{A\} = \emptyset$
3		reseq2	$⊢ \{A\} = \emptyset \to {B ↾}_{\{A\}} = {B ↾}_{\emptyset}$
4		res0	$⊢ {B ↾}_{\emptyset} = \emptyset$
5	3 4	eqtrdi	$⊢ \{A\} = \emptyset \to {B ↾}_{\{A\}} = \emptyset$
6	2 5	sylbi	$⊢ \neg A \in V \to {B ↾}_{\{A\}} = \emptyset$
7	6	necon1ai	$⊢ {B ↾}_{\{A\}} \neq \emptyset \to A \in V$
8		eleq1	$⊢ x = A \to (x \in dom B \leftrightarrow A \in dom B)$
9		sneq	$⊢ x = A \to \{x\} = \{A\}$
10	9	reseq2d	$⊢ x = A \to {B ↾}_{\{x\}} = {B ↾}_{\{A\}}$
11	10	neeq1d	$⊢ x = A \to ({B ↾}_{\{x\}} \neq \emptyset \leftrightarrow {B ↾}_{\{A\}} \neq \emptyset)$
12		dfclel	$⊢ ⟨x, y⟩ \in B \leftrightarrow \exists p (p = ⟨x, y⟩ \land p \in B)$
13	12	exbii	$⊢ \exists y ⟨x, y⟩ \in B \leftrightarrow \exists y \exists p (p = ⟨x, y⟩ \land p \in B)$
14		vex	$⊢ x \in V$
15	14	eldm2	$⊢ x \in dom B \leftrightarrow \exists y ⟨x, y⟩ \in B$
16		n0	$⊢ {B ↾}_{\{x\}} \neq \emptyset \leftrightarrow \exists p p \in ({B ↾}_{\{x\}})$
17		elres	$⊢ p \in ({B ↾}_{\{x\}}) \leftrightarrow \exists z \in \{x\} \exists y (p = ⟨z, y⟩ \land ⟨z, y⟩ \in B)$
18		eleq1	$⊢ p = ⟨z, y⟩ \to (p \in B \leftrightarrow ⟨z, y⟩ \in B)$
19	18	pm5.32i	$⊢ (p = ⟨z, y⟩ \land p \in B) \leftrightarrow (p = ⟨z, y⟩ \land ⟨z, y⟩ \in B)$
20		opeq1	$⊢ z = x \to ⟨z, y⟩ = ⟨x, y⟩$
21	20	eqeq2d	$⊢ z = x \to (p = ⟨z, y⟩ \leftrightarrow p = ⟨x, y⟩)$
22	21	anbi1d	$⊢ z = x \to ((p = ⟨z, y⟩ \land p \in B) \leftrightarrow (p = ⟨x, y⟩ \land p \in B))$
23	19 22	bitr3id	$⊢ z = x \to ((p = ⟨z, y⟩ \land ⟨z, y⟩ \in B) \leftrightarrow (p = ⟨x, y⟩ \land p \in B))$
24	23	exbidv	$⊢ z = x \to (\exists y (p = ⟨z, y⟩ \land ⟨z, y⟩ \in B) \leftrightarrow \exists y (p = ⟨x, y⟩ \land p \in B))$
25	14 24	rexsn	$⊢ \exists z \in \{x\} \exists y (p = ⟨z, y⟩ \land ⟨z, y⟩ \in B) \leftrightarrow \exists y (p = ⟨x, y⟩ \land p \in B)$
26	17 25	bitri	$⊢ p \in ({B ↾}_{\{x\}}) \leftrightarrow \exists y (p = ⟨x, y⟩ \land p \in B)$
27	26	exbii	$⊢ \exists p p \in ({B ↾}_{\{x\}}) \leftrightarrow \exists p \exists y (p = ⟨x, y⟩ \land p \in B)$
28		excom	$⊢ \exists p \exists y (p = ⟨x, y⟩ \land p \in B) \leftrightarrow \exists y \exists p (p = ⟨x, y⟩ \land p \in B)$
29	16 27 28	3bitri	$⊢ {B ↾}_{\{x\}} \neq \emptyset \leftrightarrow \exists y \exists p (p = ⟨x, y⟩ \land p \in B)$
30	13 15 29	3bitr4i	$⊢ x \in dom B \leftrightarrow {B ↾}_{\{x\}} \neq \emptyset$
31	8 11 30	vtoclbg	$⊢ A \in V \to (A \in dom B \leftrightarrow {B ↾}_{\{A\}} \neq \emptyset)$
32	1 7 31	pm5.21nii	$⊢ A \in dom B \leftrightarrow {B ↾}_{\{A\}} \neq \emptyset$

Metamath Proof Explorer

Theorem eldm3

Proof