Metamath Proof Explorer

Theorem finxpreclem1

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

		Ref	Expression
	Assertion	finxpreclem1	⊢ ( 𝑋 ∈ 𝑈 → ∅ = ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		df-ov	⊢ ( 1_o ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) 𝑋 ) = ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ )
2		eqidd	⊢ ( 𝑋 ∈ 𝑈 → ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) )
3		eleq1a	⊢ ( 𝑋 ∈ 𝑈 → ( 𝑥 = 𝑋 → 𝑥 ∈ 𝑈 ) )
4	3	anim2d	⊢ ( 𝑋 ∈ 𝑈 → ( ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) → ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) ) )
5		iftrue	⊢ ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) → if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = ∅ )
6	4 5	syl6	⊢ ( 𝑋 ∈ 𝑈 → ( ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) → if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = ∅ ) )
7	6	imp	⊢ ( ( 𝑋 ∈ 𝑈 ∧ ( 𝑛 = 1_o ∧ 𝑥 = 𝑋 ) ) → if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = ∅ )
8		1onn	⊢ 1_o ∈ ω
9	8	a1i	⊢ ( 𝑋 ∈ 𝑈 → 1_o ∈ ω )
10		elex	⊢ ( 𝑋 ∈ 𝑈 → 𝑋 ∈ V )
11		0ex	⊢ ∅ ∈ V
12	11	a1i	⊢ ( 𝑋 ∈ 𝑈 → ∅ ∈ V )
13	2 7 9 10 12	ovmpod	⊢ ( 𝑋 ∈ 𝑈 → ( 1_o ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) 𝑋 ) = ∅ )
14	1 13	syl5reqr	⊢ ( 𝑋 ∈ 𝑈 → ∅ = ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1_o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1^st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1_o , 𝑋 ⟩ ) )