bnj96

Description: Technical lemma for bnj150 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Revised by Mario Carneiro, 6-May-2015) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	bnj96.1	$⊢ F = \{⟨\emptyset, pred (x, A, R)⟩\}$
	Assertion	bnj96	$⊢ (R FrSe A \land x \in A) \to dom F = 1_{𝑜}$

Proof

Step	Hyp	Ref	Expression
1		bnj96.1	$⊢ F = \{⟨\emptyset, pred (x, A, R)⟩\}$
2		bnj93	$⊢ (R FrSe A \land x \in A) \to pred (x, A, R) \in V$
3		dmsnopg	$⊢ pred (x, A, R) \in V \to dom \{⟨\emptyset, pred (x, A, R)⟩\} = \{\emptyset\}$
4	2 3	syl	$⊢ (R FrSe A \land x \in A) \to dom \{⟨\emptyset, pred (x, A, R)⟩\} = \{\emptyset\}$
5	1	dmeqi	$⊢ dom F = dom \{⟨\emptyset, pred (x, A, R)⟩\}$
6		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
7	4 5 6	3eqtr4g	$⊢ (R FrSe A \land x \in A) \to dom F = 1_{𝑜}$

Metamath Proof Explorer

Theorem bnj96

Proof