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	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
	bnj927.2	⊢ 𝐶 ∈ V
Assertion	bnj927	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝐺 Fn 𝑝 )

Proof

Step	Hyp	Ref	Expression
1		bnj927.1	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
2		bnj927.2	⊢ 𝐶 ∈ V
3		simpr	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝑓 Fn 𝑛 )
4		vex	⊢ 𝑛 ∈ V
5	4 2	fnsn	⊢ { ⟨ 𝑛 , 𝐶 ⟩ } Fn { 𝑛 }
6	5	a1i	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → { ⟨ 𝑛 , 𝐶 ⟩ } Fn { 𝑛 } )
7		bnj521	⊢ ( 𝑛 ∩ { 𝑛 } ) = ∅
8	7	a1i	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → ( 𝑛 ∩ { 𝑛 } ) = ∅ )
9	3 6 8	fnund	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } ) Fn ( 𝑛 ∪ { 𝑛 } ) )
10	1	fneq1i	⊢ ( 𝐺 Fn ( 𝑛 ∪ { 𝑛 } ) ↔ ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } ) Fn ( 𝑛 ∪ { 𝑛 } ) )
11	9 10	sylibr	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝐺 Fn ( 𝑛 ∪ { 𝑛 } ) )
12		df-suc	⊢ suc 𝑛 = ( 𝑛 ∪ { 𝑛 } )
13	12	eqeq2i	⊢ ( 𝑝 = suc 𝑛 ↔ 𝑝 = ( 𝑛 ∪ { 𝑛 } ) )
14	13	biimpi	⊢ ( 𝑝 = suc 𝑛 → 𝑝 = ( 𝑛 ∪ { 𝑛 } ) )
15	14	adantr	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝑝 = ( 𝑛 ∪ { 𝑛 } ) )
16	15	fneq2d	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → ( 𝐺 Fn 𝑝 ↔ 𝐺 Fn ( 𝑛 ∪ { 𝑛 } ) ) )
17	11 16	mpbird	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝐺 Fn 𝑝 )