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

Proof

Step Hyp Ref Expression
1 bnj941.1 ⊢ G = f ∪ n C
2 opeq2 ⊢ C = if C ∈ V C ∅ → n C = n if C ∈ V C ∅
3 2 sneqd ⊢ C = if C ∈ V C ∅ → n C = n if C ∈ V C ∅
4 3 uneq2d ⊢ C = if C ∈ V C ∅ → f ∪ n C = f ∪ n if C ∈ V C ∅
5 1 4 eqtrid ⊢ C = if C ∈ V C ∅ → G = f ∪ n if C ∈ V C ∅
6 5 fneq1d ⊢ C = if C ∈ V C ∅ → G Fn p ↔ f ∪ n if C ∈ V C ∅ Fn p
7 6 imbi2d ⊢ C = if C ∈ V C ∅ → p = suc ⁡ n ∧ f Fn n → G Fn p ↔ p = suc ⁡ n ∧ f Fn n → f ∪ n if C ∈ V C ∅ Fn p
8 eqid ⊢ f ∪ n if C ∈ V C ∅ = f ∪ n if C ∈ V C ∅
9 0ex ⊢ ∅ ∈ V
10 9 elimel ⊢ if C ∈ V C ∅ ∈ V
11 8 10 bnj927 ⊢ p = suc ⁡ n ∧ f Fn n → f ∪ n if C ∈ V C ∅ Fn p
12 7 11 dedth ⊢ C ∈ V → p = suc ⁡ n ∧ f Fn n → G Fn p