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

Metamath Proof Explorer

Theorem bnj927

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj927.1 
|- G = ( f u. { <. n , C >. } )
bnj927.2 
|- C e. _V
Assertion bnj927 
|- ( ( p = suc n /\ f Fn n ) -> G Fn p )

Proof

Step Hyp Ref Expression
1 bnj927.1 
 |-  G = ( f u. { <. n , C >. } )
2 bnj927.2 
 |-  C e. _V
3 simpr 
 |-  ( ( p = suc n /\ f Fn n ) -> f Fn n )
4 vex 
 |-  n e. _V
5 4 2 fnsn 
 |-  { <. n , C >. } Fn { n }
6 5 a1i 
 |-  ( ( p = suc n /\ f Fn n ) -> { <. n , C >. } Fn { n } )
7 disjcsn 
 |-  ( n i^i { n } ) = (/)
8 7 a1i 
 |-  ( ( p = suc n /\ f Fn n ) -> ( n i^i { n } ) = (/) )
9 3 6 8 fnund 
 |-  ( ( p = suc n /\ f Fn n ) -> ( f u. { <. n , C >. } ) Fn ( n u. { n } ) )
10 1 fneq1i 
 |-  ( G Fn ( n u. { n } ) <-> ( f u. { <. n , C >. } ) Fn ( n u. { n } ) )
11 9 10 sylibr 
 |-  ( ( p = suc n /\ f Fn n ) -> G Fn ( n u. { n } ) )
12 df-suc 
 |-  suc n = ( n u. { n } )
13 12 eqeq2i 
 |-  ( p = suc n <-> p = ( n u. { n } ) )
14 13 biimpi 
 |-  ( p = suc n -> p = ( n u. { n } ) )
15 14 adantr 
 |-  ( ( p = suc n /\ f Fn n ) -> p = ( n u. { n } ) )
16 15 fneq2d 
 |-  ( ( p = suc n /\ f Fn n ) -> ( G Fn p <-> G Fn ( n u. { n } ) ) )
17 11 16 mpbird 
 |-  ( ( p = suc n /\ f Fn n ) -> G Fn p )