Metamath Proof Explorer

Theorem fin12

Description: Weak theorem which skips Ia but has a trivial proof, needed to prove fin1a2 . (Contributed by Stefan O'Rear, 8-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin12 
|- ( A e. Fin -> A e. Fin2 )

Proof

Step Hyp Ref Expression
1 vex 
 |-  b e. _V
2 1 a1i 
 |-  ( ( ( A e. Fin /\ b e. ~P ~P A ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> b e. _V )
3 isfin1-3 
 |-  ( A e. Fin -> ( A e. Fin <-> `' [C.] Fr ~P A ) )
4 3 ibi 
 |-  ( A e. Fin -> `' [C.] Fr ~P A )
5 4 ad2antrr 
 |-  ( ( ( A e. Fin /\ b e. ~P ~P A ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> `' [C.] Fr ~P A )
6 elpwi 
 |-  ( b e. ~P ~P A -> b C_ ~P A )
7 6 ad2antlr 
 |-  ( ( ( A e. Fin /\ b e. ~P ~P A ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> b C_ ~P A )
8 simprl 
 |-  ( ( ( A e. Fin /\ b e. ~P ~P A ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> b =/= (/) )
9 fri 
 |-  ( ( ( b e. _V /\ `' [C.] Fr ~P A ) /\ ( b C_ ~P A /\ b =/= (/) ) ) -> E. c e. b A. d e. b -. d `' [C.] c )
10 2 5 7 8 9 syl22anc 
 |-  ( ( ( A e. Fin /\ b e. ~P ~P A ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> E. c e. b A. d e. b -. d `' [C.] c )
11 vex 
 |-  d e. _V
12 vex 
 |-  c e. _V
13 11 12 brcnv 
 |-  ( d `' [C.] c <-> c [C.] d )
14 11 brrpss 
 |-  ( c [C.] d <-> c C. d )
15 13 14 bitri 
 |-  ( d `' [C.] c <-> c C. d )
16 15 notbii 
 |-  ( -. d `' [C.] c <-> -. c C. d )
17 16 ralbii 
 |-  ( A. d e. b -. d `' [C.] c <-> A. d e. b -. c C. d )
18 17 rexbii 
 |-  ( E. c e. b A. d e. b -. d `' [C.] c <-> E. c e. b A. d e. b -. c C. d )
19 10 18 sylib 
 |-  ( ( ( A e. Fin /\ b e. ~P ~P A ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> E. c e. b A. d e. b -. c C. d )
20 sorpssuni 
 |-  ( [C.] Or b -> ( E. c e. b A. d e. b -. c C. d <-> U. b e. b ) )
21 20 ad2antll 
 |-  ( ( ( A e. Fin /\ b e. ~P ~P A ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> ( E. c e. b A. d e. b -. c C. d <-> U. b e. b ) )
22 19 21 mpbid 
 |-  ( ( ( A e. Fin /\ b e. ~P ~P A ) /\ ( b =/= (/) /\ [C.] Or b ) ) -> U. b e. b )
23 22 ex 
 |-  ( ( A e. Fin /\ b e. ~P ~P A ) -> ( ( b =/= (/) /\ [C.] Or b ) -> U. b e. b ) )
24 23 ralrimiva 
 |-  ( A e. Fin -> A. b e. ~P ~P A ( ( b =/= (/) /\ [C.] Or b ) -> U. b e. b ) )
25 isfin2 
 |-  ( A e. Fin -> ( A e. Fin2 <-> A. b e. ~P ~P A ( ( b =/= (/) /\ [C.] Or b ) -> U. b e. b ) ) )
26 24 25 mpbird 
 |-  ( A e. Fin -> A e. Fin2 )