Metamath Proof Explorer

Theorem finxpreclem1

Description: Lemma for ^^ recursion theorems. (Contributed by ML, 17-Oct-2020)

Ref Expression
Assertion finxpreclem1 ⊢ X ∈ U → ∅ = n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x ⁡ 1 𝑜 X

Proof

Step Hyp Ref Expression
1 eqidd ⊢ X ∈ U → n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x = n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x
2 eleq1a ⊢ X ∈ U → x = X → x ∈ U
3 2 anim2d ⊢ X ∈ U → n = 1 𝑜 ∧ x = X → n = 1 𝑜 ∧ x ∈ U
4 iftrue ⊢ n = 1 𝑜 ∧ x ∈ U → if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x = ∅
5 3 4 syl6 ⊢ X ∈ U → n = 1 𝑜 ∧ x = X → if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x = ∅
6 5 imp ⊢ X ∈ U ∧ n = 1 𝑜 ∧ x = X → if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x = ∅
7 1onn ⊢ 1 𝑜 ∈ ω
8 7 a1i ⊢ X ∈ U → 1 𝑜 ∈ ω
9 elex ⊢ X ∈ U → X ∈ V
10 0ex ⊢ ∅ ∈ V
11 10 a1i ⊢ X ∈ U → ∅ ∈ V
12 1 6 8 9 11 ovmpod ⊢ X ∈ U → 1 𝑜 n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x X = ∅
13 df-ov ⊢ 1 𝑜 n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x X = n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x ⁡ 1 𝑜 X
14 12 13 eqtr3di ⊢ X ∈ U → ∅ = n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x ⁡ 1 𝑜 X