fnpr2o

Description: Function with a domain of 2o . (Contributed by Jim Kingdon, 25-Sep-2023)

		Ref	Expression
	Assertion	fnpr2o	$⊢ (A \in V \land B \in W) \to \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜}$

Step	Hyp	Ref	Expression
1		peano1	$⊢ \emptyset \in ω$
2	1	a1i	$⊢ (A \in V \land B \in W) \to \emptyset \in ω$
3		1onn	$⊢ 1_{𝑜} \in ω$
4	3	a1i	$⊢ (A \in V \land B \in W) \to 1_{𝑜} \in ω$
5		simpl	$⊢ (A \in V \land B \in W) \to A \in V$
6		simpr	$⊢ (A \in V \land B \in W) \to B \in W$
7		1n0	$⊢ 1_{𝑜} \neq \emptyset$
8	7	necomi	$⊢ \emptyset \neq 1_{𝑜}$
9	8	a1i	$⊢ (A \in V \land B \in W) \to \emptyset \neq 1_{𝑜}$
10		fnprg	$⊢ ((\emptyset \in ω \land 1_{𝑜} \in ω) \land (A \in V \land B \in W) \land \emptyset \neq 1_{𝑜}) \to \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn \{\emptyset, 1_{𝑜}\}$
11	2 4 5 6 9 10	syl221anc	$⊢ (A \in V \land B \in W) \to \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn \{\emptyset, 1_{𝑜}\}$
12		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
13	12	fneq2i	$⊢ \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜} \leftrightarrow \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn \{\emptyset, 1_{𝑜}\}$
14	11 13	sylibr	$⊢ (A \in V \land B \in W) \to \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜}$

Metamath Proof Explorer