Metamath Proof Explorer

Theorem fin23lem14

Description: Lemma for fin23 . U will never evolve to an empty set if it did not start with one. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Hypothesis fin23lem.a 
|- U = seqom ( ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )
Assertion fin23lem14 
|- ( ( A e. _om /\ U. ran t =/= (/) ) -> ( U ` A ) =/= (/) )

Proof

Step Hyp Ref Expression
1 fin23lem.a 
 |-  U = seqom ( ( i e. _om , u e. _V |-> if ( ( ( t ` i ) i^i u ) = (/) , u , ( ( t ` i ) i^i u ) ) ) , U. ran t )
2 fveq2 
 |-  ( a = (/) -> ( U ` a ) = ( U ` (/) ) )
3 2 neeq1d 
 |-  ( a = (/) -> ( ( U ` a ) =/= (/) <-> ( U ` (/) ) =/= (/) ) )
4 3 imbi2d 
 |-  ( a = (/) -> ( ( U. ran t =/= (/) -> ( U ` a ) =/= (/) ) <-> ( U. ran t =/= (/) -> ( U ` (/) ) =/= (/) ) ) )
5 fveq2 
 |-  ( a = b -> ( U ` a ) = ( U ` b ) )
6 5 neeq1d 
 |-  ( a = b -> ( ( U ` a ) =/= (/) <-> ( U ` b ) =/= (/) ) )
7 6 imbi2d 
 |-  ( a = b -> ( ( U. ran t =/= (/) -> ( U ` a ) =/= (/) ) <-> ( U. ran t =/= (/) -> ( U ` b ) =/= (/) ) ) )
8 fveq2 
 |-  ( a = suc b -> ( U ` a ) = ( U ` suc b ) )
9 8 neeq1d 
 |-  ( a = suc b -> ( ( U ` a ) =/= (/) <-> ( U ` suc b ) =/= (/) ) )
10 9 imbi2d 
 |-  ( a = suc b -> ( ( U. ran t =/= (/) -> ( U ` a ) =/= (/) ) <-> ( U. ran t =/= (/) -> ( U ` suc b ) =/= (/) ) ) )
11 fveq2 
 |-  ( a = A -> ( U ` a ) = ( U ` A ) )
12 11 neeq1d 
 |-  ( a = A -> ( ( U ` a ) =/= (/) <-> ( U ` A ) =/= (/) ) )
13 12 imbi2d 
 |-  ( a = A -> ( ( U. ran t =/= (/) -> ( U ` a ) =/= (/) ) <-> ( U. ran t =/= (/) -> ( U ` A ) =/= (/) ) ) )
14 vex 
 |-  t e. _V
15 14 rnex 
 |-  ran t e. _V
16 15 uniex 
 |-  U. ran t e. _V
17 1 seqom0g 
 |-  ( U. ran t e. _V -> ( U ` (/) ) = U. ran t )
18 16 17 mp1i 
 |-  ( U. ran t =/= (/) -> ( U ` (/) ) = U. ran t )
19 id 
 |-  ( U. ran t =/= (/) -> U. ran t =/= (/) )
20 18 19 eqnetrd 
 |-  ( U. ran t =/= (/) -> ( U ` (/) ) =/= (/) )
21 1 fin23lem12 
 |-  ( b e. _om -> ( U ` suc b ) = if ( ( ( t ` b ) i^i ( U ` b ) ) = (/) , ( U ` b ) , ( ( t ` b ) i^i ( U ` b ) ) ) )
22 21 adantr 
 |-  ( ( b e. _om /\ ( U ` b ) =/= (/) ) -> ( U ` suc b ) = if ( ( ( t ` b ) i^i ( U ` b ) ) = (/) , ( U ` b ) , ( ( t ` b ) i^i ( U ` b ) ) ) )
23 iftrue 
 |-  ( ( ( t ` b ) i^i ( U ` b ) ) = (/) -> if ( ( ( t ` b ) i^i ( U ` b ) ) = (/) , ( U ` b ) , ( ( t ` b ) i^i ( U ` b ) ) ) = ( U ` b ) )
24 23 adantr 
 |-  ( ( ( ( t ` b ) i^i ( U ` b ) ) = (/) /\ ( b e. _om /\ ( U ` b ) =/= (/) ) ) -> if ( ( ( t ` b ) i^i ( U ` b ) ) = (/) , ( U ` b ) , ( ( t ` b ) i^i ( U ` b ) ) ) = ( U ` b ) )
25 simprr 
 |-  ( ( ( ( t ` b ) i^i ( U ` b ) ) = (/) /\ ( b e. _om /\ ( U ` b ) =/= (/) ) ) -> ( U ` b ) =/= (/) )
26 24 25 eqnetrd 
 |-  ( ( ( ( t ` b ) i^i ( U ` b ) ) = (/) /\ ( b e. _om /\ ( U ` b ) =/= (/) ) ) -> if ( ( ( t ` b ) i^i ( U ` b ) ) = (/) , ( U ` b ) , ( ( t ` b ) i^i ( U ` b ) ) ) =/= (/) )
27 iffalse 
 |-  ( -. ( ( t ` b ) i^i ( U ` b ) ) = (/) -> if ( ( ( t ` b ) i^i ( U ` b ) ) = (/) , ( U ` b ) , ( ( t ` b ) i^i ( U ` b ) ) ) = ( ( t ` b ) i^i ( U ` b ) ) )
28 27 adantr 
 |-  ( ( -. ( ( t ` b ) i^i ( U ` b ) ) = (/) /\ ( b e. _om /\ ( U ` b ) =/= (/) ) ) -> if ( ( ( t ` b ) i^i ( U ` b ) ) = (/) , ( U ` b ) , ( ( t ` b ) i^i ( U ` b ) ) ) = ( ( t ` b ) i^i ( U ` b ) ) )
29 neqne 
 |-  ( -. ( ( t ` b ) i^i ( U ` b ) ) = (/) -> ( ( t ` b ) i^i ( U ` b ) ) =/= (/) )
30 29 adantr 
 |-  ( ( -. ( ( t ` b ) i^i ( U ` b ) ) = (/) /\ ( b e. _om /\ ( U ` b ) =/= (/) ) ) -> ( ( t ` b ) i^i ( U ` b ) ) =/= (/) )
31 28 30 eqnetrd 
 |-  ( ( -. ( ( t ` b ) i^i ( U ` b ) ) = (/) /\ ( b e. _om /\ ( U ` b ) =/= (/) ) ) -> if ( ( ( t ` b ) i^i ( U ` b ) ) = (/) , ( U ` b ) , ( ( t ` b ) i^i ( U ` b ) ) ) =/= (/) )
32 26 31 pm2.61ian 
 |-  ( ( b e. _om /\ ( U ` b ) =/= (/) ) -> if ( ( ( t ` b ) i^i ( U ` b ) ) = (/) , ( U ` b ) , ( ( t ` b ) i^i ( U ` b ) ) ) =/= (/) )
33 22 32 eqnetrd 
 |-  ( ( b e. _om /\ ( U ` b ) =/= (/) ) -> ( U ` suc b ) =/= (/) )
34 33 ex 
 |-  ( b e. _om -> ( ( U ` b ) =/= (/) -> ( U ` suc b ) =/= (/) ) )
35 34 imim2d 
 |-  ( b e. _om -> ( ( U. ran t =/= (/) -> ( U ` b ) =/= (/) ) -> ( U. ran t =/= (/) -> ( U ` suc b ) =/= (/) ) ) )
36 4 7 10 13 20 35 finds 
 |-  ( A e. _om -> ( U. ran t =/= (/) -> ( U ` A ) =/= (/) ) )
37 36 imp 
 |-  ( ( A e. _om /\ U. ran t =/= (/) ) -> ( U ` A ) =/= (/) )