Theorem prfi

Description: An unordered pair is finite. For a shorter proof using ax-un , see prfiALT . (Contributed by NM, 22-Aug-2008) Avoid ax-11 , ax-un . (Revised by BTernaryTau, 13-Jan-2025)

	Ref	Expression
Assertion	prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin

Proof

Step	Hyp	Ref	Expression
1		prprc1	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 , 𝐵 } = { 𝐵 } )
2		snfi	⊢ { 𝐵 } ∈ Fin
3	1 2	eqeltrdi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 , 𝐵 } ∈ Fin )
4		prprc2	⊢ ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } = { 𝐴 } )
5		snfi	⊢ { 𝐴 } ∈ Fin
6	4 5	eqeltrdi	⊢ ( ¬ 𝐵 ∈ V → { 𝐴 , 𝐵 } ∈ Fin )
7		2onn	⊢ 2o ∈ ω
8		simp1	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵 ) → 𝐴 ∈ V )
9		simp2	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵 ) → 𝐵 ∈ V )
10		simp3	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵 ) → ¬ 𝐴 = 𝐵 )
11	8 9 10	enpr2d	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )
12		breq2	⊢ ( 𝑥 = 2o → ( { 𝐴 , 𝐵 } ≈ 𝑥 ↔ { 𝐴 , 𝐵 } ≈ 2o ) )
13	12	rspcev	⊢ ( ( 2o ∈ ω ∧ { 𝐴 , 𝐵 } ≈ 2o ) → ∃ 𝑥 ∈ ω { 𝐴 , 𝐵 } ≈ 𝑥 )
14	7 11 13	sylancr	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵 ) → ∃ 𝑥 ∈ ω { 𝐴 , 𝐵 } ≈ 𝑥 )
15		isfi	⊢ ( { 𝐴 , 𝐵 } ∈ Fin ↔ ∃ 𝑥 ∈ ω { 𝐴 , 𝐵 } ≈ 𝑥 )
16	14 15	sylibr	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ ¬ 𝐴 = 𝐵 ) → { 𝐴 , 𝐵 } ∈ Fin )
17	16	3expia	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ¬ 𝐴 = 𝐵 → { 𝐴 , 𝐵 } ∈ Fin ) )
18		dfsn2	⊢ { 𝐴 } = { 𝐴 , 𝐴 }
19		preq2	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐴 } = { 𝐴 , 𝐵 } )
20	18 19	eqtr2id	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐴 } )
21	20 5	eqeltrdi	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } ∈ Fin )
22	17 21	pm2.61d2	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝐴 , 𝐵 } ∈ Fin )
23	3 6 22	ecase	⊢ { 𝐴 , 𝐵 } ∈ Fin