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