Theorem bnj941

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

	Ref	Expression
Hypothesis	bnj941.1	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
Assertion	bnj941	⊢ ( 𝐶 ∈ V → ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝐺 Fn 𝑝 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj941.1	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
2		opeq2	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ⟨ 𝑛 , 𝐶 ⟩ = ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ )
3	2	sneqd	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → { ⟨ 𝑛 , 𝐶 ⟩ } = { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } )
4	3	uneq2d	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } ) = ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) )
5	1 4	syl5eq	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) )
6	5	fneq1d	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ( 𝐺 Fn 𝑝 ↔ ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) Fn 𝑝 ) )
7	6	imbi2d	⊢ ( 𝐶 = if ( 𝐶 ∈ V , 𝐶 , ∅ ) → ( ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝐺 Fn 𝑝 ) ↔ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) Fn 𝑝 ) ) )
8		eqid	⊢ ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) = ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } )
9		0ex	⊢ ∅ ∈ V
10	9	elimel	⊢ if ( 𝐶 ∈ V , 𝐶 , ∅ ) ∈ V
11	8 10	bnj927	⊢ ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → ( 𝑓 ∪ { ⟨ 𝑛 , if ( 𝐶 ∈ V , 𝐶 , ∅ ) ⟩ } ) Fn 𝑝 )
12	7 11	dedth	⊢ ( 𝐶 ∈ V → ( ( 𝑝 = suc 𝑛 ∧ 𝑓 Fn 𝑛 ) → 𝐺 Fn 𝑝 ) )