This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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