Metamath Proof Explorer

Theorem xpscf

Description: Equivalent condition for the pair function to be a proper function on A . (Contributed by Mario Carneiro, 20-Aug-2015)

		Ref	Expression
	Assertion	xpscf	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} : 2_{𝑜} ⟶ A \leftrightarrow (X \in A \land Y \in A)$

Proof

Step	Hyp	Ref	Expression
1		ifid	$⊢ if (k = \emptyset, A, A) = A$
2	1	eleq2i	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in if (k = \emptyset, A, A) \leftrightarrow \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in A$
3	2	ralbii	$⊢ \forall k \in 2_{𝑜} \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in if (k = \emptyset, A, A) \leftrightarrow \forall k \in 2_{𝑜} \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in A$
4	3	anbi2i	$⊢ (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land \forall k \in 2_{𝑜} \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in if (k = \emptyset, A, A)) \leftrightarrow (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land \forall k \in 2_{𝑜} \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in A)$
5		df-3an	$⊢ (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in V \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land \forall k \in 2_{𝑜} \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in if (k = \emptyset, A, A)) \leftrightarrow ((\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in V \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜}) \land \forall k \in 2_{𝑜} \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in if (k = \emptyset, A, A))$
6		elixp2	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, A) \leftrightarrow (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in V \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land \forall k \in 2_{𝑜} \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in if (k = \emptyset, A, A))$
7		2onn	$⊢ 2_{𝑜} \in ω$
8		fnex	$⊢ (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land 2_{𝑜} \in ω) \to \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in V$
9	7 8	mpan2	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \to \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in V$
10	9	pm4.71ri	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \leftrightarrow (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in V \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜})$
11	10	anbi1i	$⊢ (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land \forall k \in 2_{𝑜} \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in if (k = \emptyset, A, A)) \leftrightarrow ((\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in V \land \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜}) \land \forall k \in 2_{𝑜} \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in if (k = \emptyset, A, A))$
12	5 6 11	3bitr4i	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, A) \leftrightarrow (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land \forall k \in 2_{𝑜} \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in if (k = \emptyset, A, A))$
13		ffnfv	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} : 2_{𝑜} ⟶ A \leftrightarrow (\{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} Fn 2_{𝑜} \land \forall k \in 2_{𝑜} \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} (k) \in A)$
14	4 12 13	3bitr4i	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, A) \leftrightarrow \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} : 2_{𝑜} ⟶ A$
15		xpsfrnel2	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} \in \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, A) \leftrightarrow (X \in A \land Y \in A)$
16	14 15	bitr3i	$⊢ \{⟨\emptyset, X⟩, ⟨1_{𝑜}, Y⟩\} : 2_{𝑜} ⟶ A \leftrightarrow (X \in A \land Y \in A)$