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		bnj521	|- ( 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 )