brwitnlem

Description: Lemma for relations which assert the existence of a witness in a two-parameter set. (Contributed by Stefan O'Rear, 25-Jan-2015) (Revised by Mario Carneiro, 23-Aug-2015)

	Ref	Expression
Hypotheses	brwitnlem.r	$⊢ R = O^{-1} [V ∖ 1_{𝑜}]$
	brwitnlem.o	$⊢ O Fn X$
Assertion	brwitnlem	$⊢ A R B \leftrightarrow A O B \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		brwitnlem.r	$⊢ R = O^{-1} [V ∖ 1_{𝑜}]$
2		brwitnlem.o	$⊢ O Fn X$
3		fvex	$⊢ O (⟨A, B⟩) \in V$
4		dif1o	$⊢ O (⟨A, B⟩) \in (V ∖ 1_{𝑜}) \leftrightarrow (O (⟨A, B⟩) \in V \land O (⟨A, B⟩) \neq \emptyset)$
5	3 4	mpbiran	$⊢ O (⟨A, B⟩) \in (V ∖ 1_{𝑜}) \leftrightarrow O (⟨A, B⟩) \neq \emptyset$
6	5	anbi2i	$⊢ (⟨A, B⟩ \in X \land O (⟨A, B⟩) \in (V ∖ 1_{𝑜})) \leftrightarrow (⟨A, B⟩ \in X \land O (⟨A, B⟩) \neq \emptyset)$
7		elpreima	$⊢ O Fn X \to (⟨A, B⟩ \in O^{-1} [V ∖ 1_{𝑜}] \leftrightarrow (⟨A, B⟩ \in X \land O (⟨A, B⟩) \in (V ∖ 1_{𝑜})))$
8	2 7	ax-mp	$⊢ ⟨A, B⟩ \in O^{-1} [V ∖ 1_{𝑜}] \leftrightarrow (⟨A, B⟩ \in X \land O (⟨A, B⟩) \in (V ∖ 1_{𝑜}))$
9		ndmfv	$⊢ \neg ⟨A, B⟩ \in dom O \to O (⟨A, B⟩) = \emptyset$
10	9	necon1ai	$⊢ O (⟨A, B⟩) \neq \emptyset \to ⟨A, B⟩ \in dom O$
11	2	fndmi	$⊢ dom O = X$
12	10 11	eleqtrdi	$⊢ O (⟨A, B⟩) \neq \emptyset \to ⟨A, B⟩ \in X$
13	12	pm4.71ri	$⊢ O (⟨A, B⟩) \neq \emptyset \leftrightarrow (⟨A, B⟩ \in X \land O (⟨A, B⟩) \neq \emptyset)$
14	6 8 13	3bitr4i	$⊢ ⟨A, B⟩ \in O^{-1} [V ∖ 1_{𝑜}] \leftrightarrow O (⟨A, B⟩) \neq \emptyset$
15	1	breqi	$⊢ A R B \leftrightarrow A O^{-1} [V ∖ 1_{𝑜}] B$
16		df-br	$⊢ A O^{-1} [V ∖ 1_{𝑜}] B \leftrightarrow ⟨A, B⟩ \in O^{-1} [V ∖ 1_{𝑜}]$
17	15 16	bitri	$⊢ A R B \leftrightarrow ⟨A, B⟩ \in O^{-1} [V ∖ 1_{𝑜}]$
18		df-ov	$⊢ A O B = O (⟨A, B⟩)$
19	18	neeq1i	$⊢ A O B \neq \emptyset \leftrightarrow O (⟨A, B⟩) \neq \emptyset$
20	14 17 19	3bitr4i	$⊢ A R B \leftrightarrow A O B \neq \emptyset$

Metamath Proof Explorer

Theorem brwitnlem

Proof