Theorem fnpr2ob

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

	Ref	Expression
Assertion	fnpr2ob	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o )

Proof

Step	Hyp	Ref	Expression
1		fnpr2o	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o )
2		0ex	⊢ ∅ ∈ V
3	2	prid1	⊢ ∅ ∈ { ∅ , 1o }
4		df2o3	⊢ 2o = { ∅ , 1o }
5	3 4	eleqtrri	⊢ ∅ ∈ 2o
6		fndm	⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → dom { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } = 2o )
7	5 6	eleqtrrid	⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → ∅ ∈ dom { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
8	2	eldm2	⊢ ( ∅ ∈ dom { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ↔ ∃ 𝑘 ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
9	7 8	sylib	⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → ∃ 𝑘 ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
10		1n0	⊢ 1o ≠ ∅
11	10	nesymi	⊢ ¬ ∅ = 1o
12		vex	⊢ 𝑘 ∈ V
13	2 12	opth1	⊢ ( ⟨ ∅ , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ → ∅ = 1o )
14	11 13	mto	⊢ ¬ ⟨ ∅ , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩
15		elpri	⊢ ( ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( ⟨ ∅ , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ∨ ⟨ ∅ , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ) )
16		orel2	⊢ ( ¬ ⟨ ∅ , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ → ( ( ⟨ ∅ , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ∨ ⟨ ∅ , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ) → ⟨ ∅ , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ) )
17	14 15 16	mpsyl	⊢ ( ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ⟨ ∅ , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ )
18	2 12	opth	⊢ ( ⟨ ∅ , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ↔ ( ∅ = ∅ ∧ 𝑘 = 𝐴 ) )
19	17 18	sylib	⊢ ( ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( ∅ = ∅ ∧ 𝑘 = 𝐴 ) )
20	19	simprd	⊢ ( ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → 𝑘 = 𝐴 )
21	20	eximi	⊢ ( ∃ 𝑘 ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ∃ 𝑘 𝑘 = 𝐴 )
22		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑘 𝑘 = 𝐴 )
23	21 22	sylibr	⊢ ( ∃ 𝑘 ⟨ ∅ , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → 𝐴 ∈ V )
24	9 23	syl	⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → 𝐴 ∈ V )
25		1oelpr	⊢ 1o ∈ { ∅ , 1o }
26	25 4	eleqtrri	⊢ 1o ∈ 2o
27	26 6	eleqtrrid	⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → 1o ∈ dom { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
28		1oex	⊢ 1o ∈ V
29	28	eldm2	⊢ ( 1o ∈ dom { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } ↔ ∃ 𝑘 ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
30	27 29	sylib	⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → ∃ 𝑘 ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } )
31	10	neii	⊢ ¬ 1o = ∅
32	28 12	opth1	⊢ ( ⟨ 1o , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ → 1o = ∅ )
33	31 32	mto	⊢ ¬ ⟨ 1o , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩
34		elpri	⊢ ( ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( ⟨ 1o , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ∨ ⟨ 1o , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ) )
35	34	orcomd	⊢ ( ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( ⟨ 1o , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ∨ ⟨ 1o , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ) )
36		orel2	⊢ ( ¬ ⟨ 1o , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ → ( ( ⟨ 1o , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ∨ ⟨ 1o , 𝑘 ⟩ = ⟨ ∅ , 𝐴 ⟩ ) → ⟨ 1o , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ) )
37	33 35 36	mpsyl	⊢ ( ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ⟨ 1o , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ )
38	28 12	opth	⊢ ( ⟨ 1o , 𝑘 ⟩ = ⟨ 1o , 𝐵 ⟩ ↔ ( 1o = 1o ∧ 𝑘 = 𝐵 ) )
39	37 38	sylib	⊢ ( ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ( 1o = 1o ∧ 𝑘 = 𝐵 ) )
40	39	simprd	⊢ ( ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → 𝑘 = 𝐵 )
41	40	eximi	⊢ ( ∃ 𝑘 ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → ∃ 𝑘 𝑘 = 𝐵 )
42		isset	⊢ ( 𝐵 ∈ V ↔ ∃ 𝑘 𝑘 = 𝐵 )
43	41 42	sylibr	⊢ ( ∃ 𝑘 ⟨ 1o , 𝑘 ⟩ ∈ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } → 𝐵 ∈ V )
44	30 43	syl	⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → 𝐵 ∈ V )
45	24 44	jca	⊢ ( { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
46	1 45	impbii	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ { ⟨ ∅ , 𝐴 ⟩ , ⟨ 1o , 𝐵 ⟩ } Fn 2o )