Theorem pr2cv

Description: If an unordered pair is equinumerous to ordinal two, then both parts are sets. (Contributed by RP, 8-Oct-2023)

	Ref	Expression
Assertion	pr2cv	⊢ ( { 𝐴 , 𝐵 } ≈ 2o → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		en2	⊢ ( { 𝐴 , 𝐵 } ≈ 2o → ∃ 𝑥 ∃ 𝑦 { 𝐴 , 𝐵 } = { 𝑥 , 𝑦 } )
2		breq1	⊢ ( { 𝐴 , 𝐵 } = { 𝑥 , 𝑦 } → ( { 𝐴 , 𝐵 } ≈ 2o ↔ { 𝑥 , 𝑦 } ≈ 2o ) )
3		vex	⊢ 𝑥 ∈ V
4		vex	⊢ 𝑦 ∈ V
5		pr2ne	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( { 𝑥 , 𝑦 } ≈ 2o ↔ 𝑥 ≠ 𝑦 ) )
6	5	el2v	⊢ ( { 𝑥 , 𝑦 } ≈ 2o ↔ 𝑥 ≠ 𝑦 )
7	6	biimpi	⊢ ( { 𝑥 , 𝑦 } ≈ 2o → 𝑥 ≠ 𝑦 )
8		preq12nebg	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑥 ≠ 𝑦 ) → ( { 𝑥 , 𝑦 } = { 𝐴 , 𝐵 } ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐴 ) ) ) )
9		eqvisset	⊢ ( 𝑥 = 𝐴 → 𝐴 ∈ V )
10		eqvisset	⊢ ( 𝑦 = 𝐵 → 𝐵 ∈ V )
11	9 10	anim12i	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
12		eqvisset	⊢ ( 𝑥 = 𝐵 → 𝐵 ∈ V )
13		eqvisset	⊢ ( 𝑦 = 𝐴 → 𝐴 ∈ V )
14	12 13	anim12ci	⊢ ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐴 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
15	11 14	jaoi	⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐴 ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
16	8 15	syl6bi	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑥 ≠ 𝑦 ) → ( { 𝑥 , 𝑦 } = { 𝐴 , 𝐵 } → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
17	3 4 7 16	mp3an12i	⊢ ( { 𝑥 , 𝑦 } ≈ 2o → ( { 𝑥 , 𝑦 } = { 𝐴 , 𝐵 } → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
18	17	com12	⊢ ( { 𝑥 , 𝑦 } = { 𝐴 , 𝐵 } → ( { 𝑥 , 𝑦 } ≈ 2o → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
19	18	eqcoms	⊢ ( { 𝐴 , 𝐵 } = { 𝑥 , 𝑦 } → ( { 𝑥 , 𝑦 } ≈ 2o → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
20	2 19	sylbid	⊢ ( { 𝐴 , 𝐵 } = { 𝑥 , 𝑦 } → ( { 𝐴 , 𝐵 } ≈ 2o → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
21	20	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 { 𝐴 , 𝐵 } = { 𝑥 , 𝑦 } → ( { 𝐴 , 𝐵 } ≈ 2o → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) )
22	1 21	mpcom	⊢ ( { 𝐴 , 𝐵 } ≈ 2o → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )