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

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝐶 = 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 𝑝 ) )