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 ⊢ A B ∈ Fin

Proof

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