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

Metamath Proof Explorer

Theorem tfrlem10

Description: Lemma for transfinite recursion. We define class C by extending recs with one ordered pair. We will assume, falsely, that domain of recs is a member of, and thus not equal to, On . Using this assumption we will prove facts about C that will lead to a contradiction in tfrlem14 , thus showing the domain of recs does in fact equal On . Here we show (under the false assumption) that C is a function extending the domain of recs ( F ) by one. (Contributed by NM, 14-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypotheses tfrlem.1 
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
tfrlem.3 
|- C = ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
Assertion tfrlem10 
|- ( dom recs ( F ) e. On -> C Fn suc dom recs ( F ) )

Proof

Step Hyp Ref Expression
1 tfrlem.1 
 |-  A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
2 tfrlem.3 
 |-  C = ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
3 fvex 
 |-  ( F ` recs ( F ) ) e. _V
4 funsng 
 |-  ( ( dom recs ( F ) e. On /\ ( F ` recs ( F ) ) e. _V ) -> Fun { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
5 3 4 mpan2 
 |-  ( dom recs ( F ) e. On -> Fun { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
6 1 tfrlem7 
 |-  Fun recs ( F )
7 5 6 jctil 
 |-  ( dom recs ( F ) e. On -> ( Fun recs ( F ) /\ Fun { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) )
8 3 dmsnop 
 |-  dom { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } = { dom recs ( F ) }
9 8 ineq2i 
 |-  ( dom recs ( F ) i^i dom { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = ( dom recs ( F ) i^i { dom recs ( F ) } )
10 1 tfrlem8 
 |-  Ord dom recs ( F )
11 orddisj 
 |-  ( Ord dom recs ( F ) -> ( dom recs ( F ) i^i { dom recs ( F ) } ) = (/) )
12 10 11 ax-mp 
 |-  ( dom recs ( F ) i^i { dom recs ( F ) } ) = (/)
13 9 12 eqtri 
 |-  ( dom recs ( F ) i^i dom { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = (/)
14 funun 
 |-  ( ( ( Fun recs ( F ) /\ Fun { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) /\ ( dom recs ( F ) i^i dom { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = (/) ) -> Fun ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) )
15 7 13 14 sylancl 
 |-  ( dom recs ( F ) e. On -> Fun ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) )
16 8 uneq2i 
 |-  ( dom recs ( F ) u. dom { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = ( dom recs ( F ) u. { dom recs ( F ) } )
17 dmun 
 |-  dom ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = ( dom recs ( F ) u. dom { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
18 df-suc 
 |-  suc dom recs ( F ) = ( dom recs ( F ) u. { dom recs ( F ) } )
19 16 17 18 3eqtr4i 
 |-  dom ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = suc dom recs ( F )
20 df-fn 
 |-  ( ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) Fn suc dom recs ( F ) <-> ( Fun ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) /\ dom ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = suc dom recs ( F ) ) )
21 15 19 20 sylanblrc 
 |-  ( dom recs ( F ) e. On -> ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) Fn suc dom recs ( F ) )
22 2 fneq1i 
 |-  ( C Fn suc dom recs ( F ) <-> ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) Fn suc dom recs ( F ) )
23 21 22 sylibr 
 |-  ( dom recs ( F ) e. On -> C Fn suc dom recs ( F ) )