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 ⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
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 disjcsn ⊢ ( 𝑛 ∩ { 𝑛 } ) = ∅
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 𝑝 )