Metamath Proof Explorer

Theorem finxpreclem3

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

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

Proof

Step Hyp Ref Expression
1 finxpreclem3.1 ⊢ 𝐹 = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
2 1 a1i ⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑋 ∈ ( V × 𝑈 ) ) → 𝐹 = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) )
3 eqeq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 = 1o ↔ 𝑁 = 1o ) )
4 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈 ) )
5 3 4 bi2anan9 ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) ↔ ( 𝑁 = 1o ∧ 𝑋 ∈ 𝑈 ) ) )
6 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ ( V × 𝑈 ) ↔ 𝑋 ∈ ( V × 𝑈 ) ) )
7 6 adantl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( 𝑥 ∈ ( V × 𝑈 ) ↔ 𝑋 ∈ ( V × 𝑈 ) ) )
8 unieq ⊢ ( 𝑛 = 𝑁 → ∪ 𝑛 = ∪ 𝑁 )
9 8 adantr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ∪ 𝑛 = ∪ 𝑁 )
10 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑋 ) )
11 10 adantl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑋 ) )
12 9 11 opeq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ = ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ )
13 opeq12 ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ⟨ 𝑛 , 𝑥 ⟩ = ⟨ 𝑁 , 𝑋 ⟩ )
14 7 12 13 ifbieq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) = if ( 𝑋 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ , ⟨ 𝑁 , 𝑋 ⟩ ) )
15 5 14 ifbieq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = if ( ( 𝑁 = 1o ∧ 𝑋 ∈ 𝑈 ) , ∅ , if ( 𝑋 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ , ⟨ 𝑁 , 𝑋 ⟩ ) ) )
16 sssucid ⊢ 1o ⊆ suc 1o
17 df-2o ⊢ 2o = suc 1o
18 16 17 sseqtrri ⊢ 1o ⊆ 2o
19 1on ⊢ 1o ∈ On
20 17 19 sucneqoni ⊢ 2o ≠ 1o
21 20 necomi ⊢ 1o ≠ 2o
22 df-pss ⊢ ( 1o ⊊ 2o ↔ ( 1o ⊆ 2o ∧ 1o ≠ 2o ) )
23 18 21 22 mpbir2an ⊢ 1o ⊊ 2o
24 ssnpss ⊢ ( 2o ⊆ 1o → ¬ 1o ⊊ 2o )
25 23 24 mt2 ⊢ ¬ 2o ⊆ 1o
26 sseq2 ⊢ ( 𝑁 = 1o → ( 2o ⊆ 𝑁 ↔ 2o ⊆ 1o ) )
27 25 26 mtbiri ⊢ ( 𝑁 = 1o → ¬ 2o ⊆ 𝑁 )
28 27 con2i ⊢ ( 2o ⊆ 𝑁 → ¬ 𝑁 = 1o )
29 28 intnanrd ⊢ ( 2o ⊆ 𝑁 → ¬ ( 𝑁 = 1o ∧ 𝑋 ∈ 𝑈 ) )
30 29 iffalsed ⊢ ( 2o ⊆ 𝑁 → if ( ( 𝑁 = 1o ∧ 𝑋 ∈ 𝑈 ) , ∅ , if ( 𝑋 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ , ⟨ 𝑁 , 𝑋 ⟩ ) ) = if ( 𝑋 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ , ⟨ 𝑁 , 𝑋 ⟩ ) )
31 iftrue ⊢ ( 𝑋 ∈ ( V × 𝑈 ) → if ( 𝑋 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ , ⟨ 𝑁 , 𝑋 ⟩ ) = ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ )
32 30 31 sylan9eq ⊢ ( ( 2o ⊆ 𝑁 ∧ 𝑋 ∈ ( V × 𝑈 ) ) → if ( ( 𝑁 = 1o ∧ 𝑋 ∈ 𝑈 ) , ∅ , if ( 𝑋 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ , ⟨ 𝑁 , 𝑋 ⟩ ) ) = ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ )
33 15 32 sylan9eqr ⊢ ( ( ( 2o ⊆ 𝑁 ∧ 𝑋 ∈ ( V × 𝑈 ) ) ∧ ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) ) → if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ )
34 33 adantlll ⊢ ( ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑋 ∈ ( V × 𝑈 ) ) ∧ ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) ) → if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) = ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ )
35 simpll ⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑋 ∈ ( V × 𝑈 ) ) → 𝑁 ∈ ω )
36 elex ⊢ ( 𝑋 ∈ ( V × 𝑈 ) → 𝑋 ∈ V )
37 36 adantl ⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑋 ∈ ( V × 𝑈 ) ) → 𝑋 ∈ V )
38 opex ⊢ ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ ∈ V
39 38 a1i ⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑋 ∈ ( V × 𝑈 ) ) → ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ ∈ V )
40 2 34 35 37 39 ovmpod ⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑋 ∈ ( V × 𝑈 ) ) → ( 𝑁 𝐹 𝑋 ) = ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ )
41 df-ov ⊢ ( 𝑁 𝐹 𝑋 ) = ( 𝐹 ‘ ⟨ 𝑁 , 𝑋 ⟩ )
42 40 41 eqtr3di ⊢ ( ( ( 𝑁 ∈ ω ∧ 2o ⊆ 𝑁 ) ∧ 𝑋 ∈ ( V × 𝑈 ) ) → ⟨ ∪ 𝑁 , ( 1st ‘ 𝑋 ) ⟩ = ( 𝐹 ‘ ⟨ 𝑁 , 𝑋 ⟩ ) )