Theorem finxpreclem5

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

	Ref	Expression
Hypothesis	finxpreclem5.1	⊢ 𝐹 = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
Assertion	finxpreclem5	⊢ ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) → ( ¬ 𝑥 ∈ ( V × 𝑈 ) → ( 𝐹 ‘ ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ 𝑛 , 𝑥 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		finxpreclem5.1	⊢ 𝐹 = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
2		df-ov	⊢ ( 𝑛 𝐹 𝑥 ) = ( 𝐹 ‘ ⟨ 𝑛 , 𝑥 ⟩ )
3		vex	⊢ 𝑥 ∈ V
4		0ex	⊢ ∅ ∈ V
5		opex	⊢ ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ ∈ V
6		opex	⊢ ⟨ 𝑛 , 𝑥 ⟩ ∈ V
7	5 6	ifex	⊢ if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ∈ V
8	4 7	ifex	⊢ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ∈ V
9	1	ovmpt4g	⊢ ( ( 𝑛 ∈ ω ∧ 𝑥 ∈ V ∧ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ∈ V ) → ( 𝑛 𝐹 𝑥 ) = if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
10	3 8 9	mp3an23	⊢ ( 𝑛 ∈ ω → ( 𝑛 𝐹 𝑥 ) = if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
11	10	ad2antrr	⊢ ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( 𝑛 𝐹 𝑥 ) = if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
12		1on	⊢ 1o ∈ On
13	12	onirri	⊢ ¬ 1o ∈ 1o
14		eleq2	⊢ ( 𝑛 = 1o → ( 1o ∈ 𝑛 ↔ 1o ∈ 1o ) )
15	13 14	mtbiri	⊢ ( 𝑛 = 1o → ¬ 1o ∈ 𝑛 )
16	15	con2i	⊢ ( 1o ∈ 𝑛 → ¬ 𝑛 = 1o )
17	16	intnanrd	⊢ ( 1o ∈ 𝑛 → ¬ ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) )
18	17	iffalsed	⊢ ( 1o ∈ 𝑛 → if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) )
19	18	adantl	⊢ ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) → if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) )
20		iffalse	⊢ ( ¬ 𝑥 ∈ ( V × 𝑈 ) → if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ 𝑛 , 𝑥 ⟩ )
21	19 20	sylan9eq	⊢ ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = ⟨ 𝑛 , 𝑥 ⟩ )
22	11 21	eqtrd	⊢ ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( 𝑛 𝐹 𝑥 ) = ⟨ 𝑛 , 𝑥 ⟩ )
23	2 22	eqtr3id	⊢ ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( 𝐹 ‘ ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ 𝑛 , 𝑥 ⟩ )
24	23	ex	⊢ ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) → ( ¬ 𝑥 ∈ ( V × 𝑈 ) → ( 𝐹 ‘ ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ 𝑛 , 𝑥 ⟩ ) )