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 } e. Fin

Proof

Step Hyp Ref Expression
1 prprc1 
 |-  ( -. A e. _V -> { A , B } = { B } )
2 snfi 
 |-  { B } e. Fin
3 1 2 eqeltrdi 
 |-  ( -. A e. _V -> { A , B } e. Fin )
4 prprc2 
 |-  ( -. B e. _V -> { A , B } = { A } )
5 snfi 
 |-  { A } e. Fin
6 4 5 eqeltrdi 
 |-  ( -. B e. _V -> { A , B } e. Fin )
7 2onn 
 |-  2o e. _om
8 simp1 
 |-  ( ( A e. _V /\ B e. _V /\ -. A = B ) -> A e. _V )
9 simp2 
 |-  ( ( A e. _V /\ B e. _V /\ -. A = B ) -> B e. _V )
10 simp3 
 |-  ( ( A e. _V /\ B e. _V /\ -. A = B ) -> -. A = B )
11 8 9 10 enpr2d 
 |-  ( ( A e. _V /\ B e. _V /\ -. A = B ) -> { A , B } ~~ 2o )
12 breq2 
 |-  ( x = 2o -> ( { A , B } ~~ x <-> { A , B } ~~ 2o ) )
13 12 rspcev 
 |-  ( ( 2o e. _om /\ { A , B } ~~ 2o ) -> E. x e. _om { A , B } ~~ x )
14 7 11 13 sylancr 
 |-  ( ( A e. _V /\ B e. _V /\ -. A = B ) -> E. x e. _om { A , B } ~~ x )
15 isfi 
 |-  ( { A , B } e. Fin <-> E. x e. _om { A , B } ~~ x )
16 14 15 sylibr 
 |-  ( ( A e. _V /\ B e. _V /\ -. A = B ) -> { A , B } e. Fin )
17 16 3expia 
 |-  ( ( A e. _V /\ B e. _V ) -> ( -. A = B -> { A , B } e. 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 } e. Fin )
22 17 21 pm2.61d2 
 |-  ( ( A e. _V /\ B e. _V ) -> { A , B } e. Fin )
23 3 6 22 ecase 
 |-  { A , B } e. Fin