fnpr2ob

Description: Biconditional version of fnpr2o . (Contributed by Jim Kingdon, 27-Sep-2023)

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

Proof

Step	Hyp	Ref	Expression
1		fnpr2o	$⊢ (A \in V \land B \in V) \to \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜}$
2		0ex	$⊢ \emptyset \in V$
3	2	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
4		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
5	3 4	eleqtrri	$⊢ \emptyset \in 2_{𝑜}$
6		fndm	$⊢ \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜} \to dom \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} = 2_{𝑜}$
7	5 6	eleqtrrid	$⊢ \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜} \to \emptyset \in dom \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\}$
8	2	eldm2	$⊢ \emptyset \in dom \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \leftrightarrow \exists k ⟨\emptyset, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\}$
9	7 8	sylib	$⊢ \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜} \to \exists k ⟨\emptyset, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\}$
10		1n0	$⊢ 1_{𝑜} \neq \emptyset$
11	10	nesymi	$⊢ \neg \emptyset = 1_{𝑜}$
12		vex	$⊢ k \in V$
13	2 12	opth1	$⊢ ⟨\emptyset, k⟩ = ⟨1_{𝑜}, B⟩ \to \emptyset = 1_{𝑜}$
14	11 13	mto	$⊢ \neg ⟨\emptyset, k⟩ = ⟨1_{𝑜}, B⟩$
15		elpri	$⊢ ⟨\emptyset, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to (⟨\emptyset, k⟩ = ⟨\emptyset, A⟩ \lor ⟨\emptyset, k⟩ = ⟨1_{𝑜}, B⟩)$
16		orel2	$⊢ \neg ⟨\emptyset, k⟩ = ⟨1_{𝑜}, B⟩ \to ((⟨\emptyset, k⟩ = ⟨\emptyset, A⟩ \lor ⟨\emptyset, k⟩ = ⟨1_{𝑜}, B⟩) \to ⟨\emptyset, k⟩ = ⟨\emptyset, A⟩)$
17	14 15 16	mpsyl	$⊢ ⟨\emptyset, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to ⟨\emptyset, k⟩ = ⟨\emptyset, A⟩$
18	2 12	opth	$⊢ ⟨\emptyset, k⟩ = ⟨\emptyset, A⟩ \leftrightarrow (\emptyset = \emptyset \land k = A)$
19	17 18	sylib	$⊢ ⟨\emptyset, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to (\emptyset = \emptyset \land k = A)$
20	19	simprd	$⊢ ⟨\emptyset, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to k = A$
21	20	eximi	$⊢ \exists k ⟨\emptyset, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to \exists k k = A$
22		isset	$⊢ A \in V \leftrightarrow \exists k k = A$
23	21 22	sylibr	$⊢ \exists k ⟨\emptyset, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to A \in V$
24	9 23	syl	$⊢ \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜} \to A \in V$
25		1oex	$⊢ 1_{𝑜} \in V$
26	25	prid2	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
27	26 4	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
28	27 6	eleqtrrid	$⊢ \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜} \to 1_{𝑜} \in dom \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\}$
29	25	eldm2	$⊢ 1_{𝑜} \in dom \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \leftrightarrow \exists k ⟨1_{𝑜}, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\}$
30	28 29	sylib	$⊢ \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜} \to \exists k ⟨1_{𝑜}, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\}$
31	10	neii	$⊢ \neg 1_{𝑜} = \emptyset$
32	25 12	opth1	$⊢ ⟨1_{𝑜}, k⟩ = ⟨\emptyset, A⟩ \to 1_{𝑜} = \emptyset$
33	31 32	mto	$⊢ \neg ⟨1_{𝑜}, k⟩ = ⟨\emptyset, A⟩$
34		elpri	$⊢ ⟨1_{𝑜}, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to (⟨1_{𝑜}, k⟩ = ⟨\emptyset, A⟩ \lor ⟨1_{𝑜}, k⟩ = ⟨1_{𝑜}, B⟩)$
35	34	orcomd	$⊢ ⟨1_{𝑜}, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to (⟨1_{𝑜}, k⟩ = ⟨1_{𝑜}, B⟩ \lor ⟨1_{𝑜}, k⟩ = ⟨\emptyset, A⟩)$
36		orel2	$⊢ \neg ⟨1_{𝑜}, k⟩ = ⟨\emptyset, A⟩ \to ((⟨1_{𝑜}, k⟩ = ⟨1_{𝑜}, B⟩ \lor ⟨1_{𝑜}, k⟩ = ⟨\emptyset, A⟩) \to ⟨1_{𝑜}, k⟩ = ⟨1_{𝑜}, B⟩)$
37	33 35 36	mpsyl	$⊢ ⟨1_{𝑜}, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to ⟨1_{𝑜}, k⟩ = ⟨1_{𝑜}, B⟩$
38	25 12	opth	$⊢ ⟨1_{𝑜}, k⟩ = ⟨1_{𝑜}, B⟩ \leftrightarrow (1_{𝑜} = 1_{𝑜} \land k = B)$
39	37 38	sylib	$⊢ ⟨1_{𝑜}, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to (1_{𝑜} = 1_{𝑜} \land k = B)$
40	39	simprd	$⊢ ⟨1_{𝑜}, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to k = B$
41	40	eximi	$⊢ \exists k ⟨1_{𝑜}, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to \exists k k = B$
42		isset	$⊢ B \in V \leftrightarrow \exists k k = B$
43	41 42	sylibr	$⊢ \exists k ⟨1_{𝑜}, k⟩ \in \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} \to B \in V$
44	30 43	syl	$⊢ \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜} \to B \in V$
45	24 44	jca	$⊢ \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜} \to (A \in V \land B \in V)$
46	1 45	impbii	$⊢ (A \in V \land B \in V) \leftrightarrow \{⟨\emptyset, A⟩, ⟨1_{𝑜}, B⟩\} Fn 2_{𝑜}$

Metamath Proof Explorer

Theorem fnpr2ob

Proof