Metamath Proof Explorer

Theorem xpsfrnel2

Description: Elementhood in the target space of the function F appearing in xpsval . (Contributed by Mario Carneiro, 15-Aug-2015)

		Ref	Expression
	Assertion	xpsfrnel2	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \leftrightarrow (X \in A \land Y \in B)$

Proof

Step	Hyp	Ref	Expression
1		xpsfrnel	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \leftrightarrow (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (\emptyset) \in A \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (1_{𝑜}) \in B)$
2		fnpr2ob	$⊢ (X \in V \land Y \in V) \leftrightarrow \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜}$
3	2	biimpri	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \to (X \in V \land Y \in V)$
4	3	3ad2ant1	$⊢ (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (\emptyset) \in A \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (1_{𝑜}) \in B) \to (X \in V \land Y \in V)$
5		elex	$⊢ X \in A \to X \in V$
6		elex	$⊢ Y \in B \to Y \in V$
7	5 6	anim12i	$⊢ (X \in A \land Y \in B) \to (X \in V \land Y \in V)$
8		3anass	$⊢ (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (\emptyset) \in A \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (1_{𝑜}) \in B) \leftrightarrow (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (\emptyset) \in A \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (1_{𝑜}) \in B))$
9		fnpr2o	$⊢ (X \in V \land Y \in V) \to \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜}$
10	9	biantrurd	$⊢ (X \in V \land Y \in V) \to ((\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (\emptyset) \in A \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (1_{𝑜}) \in B) \leftrightarrow (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (\emptyset) \in A \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (1_{𝑜}) \in B)))$
11		fvpr0o	$⊢ X \in V \to \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (\emptyset) = X$
12	11	eleq1d	$⊢ X \in V \to (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (\emptyset) \in A \leftrightarrow X \in A)$
13		fvpr1o	$⊢ Y \in V \to \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (1_{𝑜}) = Y$
14	13	eleq1d	$⊢ Y \in V \to (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (1_{𝑜}) \in B \leftrightarrow Y \in B)$
15	12 14	bi2anan9	$⊢ (X \in V \land Y \in V) \to ((\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (\emptyset) \in A \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (1_{𝑜}) \in B) \leftrightarrow (X \in A \land Y \in B))$
16	10 15	bitr3d	$⊢ (X \in V \land Y \in V) \to ((\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (\emptyset) \in A \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (1_{𝑜}) \in B)) \leftrightarrow (X \in A \land Y \in B))$
17	8 16	syl5bb	$⊢ (X \in V \land Y \in V) \to ((\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (\emptyset) \in A \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (1_{𝑜}) \in B) \leftrightarrow (X \in A \land Y \in B))$
18	4 7 17	pm5.21nii	$⊢ (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (\emptyset) \in A \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (1_{𝑜}) \in B) \leftrightarrow (X \in A \land Y \in B)$
19	1 18	bitri	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \leftrightarrow (X \in A \land Y \in B)$