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 ⊢ G = f ∪ n C
bnj927.2 ⊢ C ∈ V
Assertion bnj927 ⊢ p = suc ⁡ n ∧ f Fn n → G Fn p

Proof

Step Hyp Ref Expression
1 bnj927.1 ⊢ G = f ∪ n C
2 bnj927.2 ⊢ C ∈ V
3 simpr ⊢ p = suc ⁡ n ∧ f Fn n → f Fn n
4 vex ⊢ n ∈ 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 ∩ n = ∅
8 7 a1i ⊢ p = suc ⁡ n ∧ f Fn n → n ∩ n = ∅
9 3 6 8 fnund ⊢ p = suc ⁡ n ∧ f Fn n → f ∪ n C Fn n ∪ n
10 1 fneq1i ⊢ G Fn n ∪ n ↔ f ∪ n C Fn n ∪ n
11 9 10 sylibr ⊢ p = suc ⁡ n ∧ f Fn n → G Fn n ∪ n
12 df-suc ⊢ suc ⁡ n = n ∪ n
13 12 eqeq2i ⊢ p = suc ⁡ n ↔ p = n ∪ n
14 13 biimpi ⊢ p = suc ⁡ n → p = n ∪ n
15 14 adantr ⊢ p = suc ⁡ n ∧ f Fn n → p = n ∪ n
16 15 fneq2d ⊢ p = suc ⁡ n ∧ f Fn n → G Fn p ↔ G Fn n ∪ n
17 11 16 mpbird ⊢ p = suc ⁡ n ∧ f Fn n → G Fn p