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 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
2 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
3 eleq1a ⊢ X ∈ U → x = X → x ∈ U
4 3 anim2d ⊢ X ∈ U → n = 1 𝑜 ∧ x = X → n = 1 𝑜 ∧ x ∈ U
5 iftrue ⊢ n = 1 𝑜 ∧ x ∈ U → if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x = ∅
6 4 5 syl6 ⊢ X ∈ U → n = 1 𝑜 ∧ x = X → if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x = ∅
7 6 imp ⊢ X ∈ U ∧ n = 1 𝑜 ∧ x = X → if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x = ∅
8 1onn ⊢ 1 𝑜 ∈ ω
9 8 a1i ⊢ X ∈ U → 1 𝑜 ∈ ω
10 elex ⊢ X ∈ U → X ∈ V
11 0ex ⊢ ∅ ∈ V
12 11 a1i ⊢ X ∈ U → ∅ ∈ V
13 2 7 9 10 12 ovmpod ⊢ X ∈ U → 1 𝑜 n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x X = ∅
14 1 13 syl5reqr ⊢ X ∈ U → ∅ = n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x ⁡ 1 𝑜 X