Metamath Proof Explorer

Theorem finxpreclem6

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

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

Proof

Step Hyp Ref Expression
1 finxpreclem5.1 ⊢ 𝐹 = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
2 eleq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∈ ω ↔ 𝑁 ∈ ω ) )
3 eleq2 ⊢ ( 𝑛 = 𝑁 → ( 1o ∈ 𝑛 ↔ 1o ∈ 𝑁 ) )
4 2 3 anbi12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ↔ ( 𝑁 ∈ ω ∧ 1o ∈ 𝑁 ) ) )
5 anass ⊢ ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) ↔ ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) ) )
6 nfv ⊢ Ⅎ 𝑥 ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) )
7 nfmpo2 ⊢ Ⅎ 𝑥 ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
8 1 7 nfcxfr ⊢ Ⅎ 𝑥 𝐹
9 nfcv ⊢ Ⅎ 𝑥 ⟨ 𝑛 , 𝑦 ⟩
10 8 9 nfrdg ⊢ Ⅎ 𝑥 rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ )
11 nfcv ⊢ Ⅎ 𝑥 𝑛
12 10 11 nffv ⊢ Ⅎ 𝑥 ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 )
13 12 nfeq2 ⊢ Ⅎ 𝑥 ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 )
14 13 nfn ⊢ Ⅎ 𝑥 ¬ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 )
15 6 14 nfim ⊢ Ⅎ 𝑥 ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) ) → ¬ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) )
16 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( V × 𝑈 ) ↔ 𝑦 ∈ ( V × 𝑈 ) ) )
17 16 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ ( V × 𝑈 ) ↔ ¬ 𝑦 ∈ ( V × 𝑈 ) ) )
18 17 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 1o ∈ 𝑛 ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ↔ ( 1o ∈ 𝑛 ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) ) )
19 18 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ) ↔ ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) ) ) )
20 opeq2 ⊢ ( 𝑥 = 𝑦 → ⟨ 𝑛 , 𝑥 ⟩ = ⟨ 𝑛 , 𝑦 ⟩ )
21 rdgeq2 ⊢ ( ⟨ 𝑛 , 𝑥 ⟩ = ⟨ 𝑛 , 𝑦 ⟩ → rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) = rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) )
22 20 21 syl ⊢ ( 𝑥 = 𝑦 → rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) = rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) )
23 22 fveq1d ⊢ ( 𝑥 = 𝑦 → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) )
24 23 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) ↔ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) )
25 24 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) ↔ ¬ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) )
26 19 25 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ) → ¬ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) ) ↔ ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) ) → ¬ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) ) )
27 anass ⊢ ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ↔ ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ) )
28 vex ⊢ 𝑛 ∈ V
29 fveqeq2 ⊢ ( 𝑚 = ∅ → ( ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑚 ) = ⟨ 𝑛 , 𝑥 ⟩ ↔ ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ ∅ ) = ⟨ 𝑛 , 𝑥 ⟩ ) )
30 fveqeq2 ⊢ ( 𝑚 = 𝑜 → ( ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑚 ) = ⟨ 𝑛 , 𝑥 ⟩ ↔ ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑜 ) = ⟨ 𝑛 , 𝑥 ⟩ ) )
31 fveqeq2 ⊢ ( 𝑚 = suc 𝑜 → ( ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑚 ) = ⟨ 𝑛 , 𝑥 ⟩ ↔ ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ suc 𝑜 ) = ⟨ 𝑛 , 𝑥 ⟩ ) )
32 opex ⊢ ⟨ 𝑛 , 𝑥 ⟩ ∈ V
33 32 rdg0 ⊢ ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ ∅ ) = ⟨ 𝑛 , 𝑥 ⟩
34 33 a1i ⊢ ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ ∅ ) = ⟨ 𝑛 , 𝑥 ⟩ )
35 nnon ⊢ ( 𝑜 ∈ ω → 𝑜 ∈ On )
36 rdgsuc ⊢ ( 𝑜 ∈ On → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ suc 𝑜 ) = ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑜 ) ) )
37 35 36 syl ⊢ ( 𝑜 ∈ ω → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ suc 𝑜 ) = ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑜 ) ) )
38 fveq2 ⊢ ( ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑜 ) = ⟨ 𝑛 , 𝑥 ⟩ → ( 𝐹 ‘ ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑜 ) ) = ( 𝐹 ‘ ⟨ 𝑛 , 𝑥 ⟩ ) )
39 37 38 sylan9eq ⊢ ( ( 𝑜 ∈ ω ∧ ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑜 ) = ⟨ 𝑛 , 𝑥 ⟩ ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ suc 𝑜 ) = ( 𝐹 ‘ ⟨ 𝑛 , 𝑥 ⟩ ) )
40 1 finxpreclem5 ⊢ ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) → ( ¬ 𝑥 ∈ ( V × 𝑈 ) → ( 𝐹 ‘ ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ 𝑛 , 𝑥 ⟩ ) )
41 40 imp ⊢ ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( 𝐹 ‘ ⟨ 𝑛 , 𝑥 ⟩ ) = ⟨ 𝑛 , 𝑥 ⟩ )
42 39 41 sylan9eq ⊢ ( ( ( 𝑜 ∈ ω ∧ ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑜 ) = ⟨ 𝑛 , 𝑥 ⟩ ) ∧ ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ suc 𝑜 ) = ⟨ 𝑛 , 𝑥 ⟩ )
43 42 expl ⊢ ( 𝑜 ∈ ω → ( ( ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑜 ) = ⟨ 𝑛 , 𝑥 ⟩ ∧ ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ suc 𝑜 ) = ⟨ 𝑛 , 𝑥 ⟩ ) )
44 43 expcomd ⊢ ( 𝑜 ∈ ω → ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑜 ) = ⟨ 𝑛 , 𝑥 ⟩ → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ suc 𝑜 ) = ⟨ 𝑛 , 𝑥 ⟩ ) ) )
45 29 30 31 34 44 finds2 ⊢ ( 𝑚 ∈ ω → ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑚 ) = ⟨ 𝑛 , 𝑥 ⟩ ) )
46 eleq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 ∈ ω ↔ 𝑚 ∈ ω ) )
47 fveqeq2 ⊢ ( 𝑛 = 𝑚 → ( ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) = ⟨ 𝑛 , 𝑥 ⟩ ↔ ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑚 ) = ⟨ 𝑛 , 𝑥 ⟩ ) )
48 47 imbi2d ⊢ ( 𝑛 = 𝑚 → ( ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) = ⟨ 𝑛 , 𝑥 ⟩ ) ↔ ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑚 ) = ⟨ 𝑛 , 𝑥 ⟩ ) ) )
49 46 48 imbi12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝑛 ∈ ω → ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) = ⟨ 𝑛 , 𝑥 ⟩ ) ) ↔ ( 𝑚 ∈ ω → ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑚 ) = ⟨ 𝑛 , 𝑥 ⟩ ) ) ) )
50 45 49 mpbiri ⊢ ( 𝑛 = 𝑚 → ( 𝑛 ∈ ω → ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) = ⟨ 𝑛 , 𝑥 ⟩ ) ) )
51 50 equcoms ⊢ ( 𝑚 = 𝑛 → ( 𝑛 ∈ ω → ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) = ⟨ 𝑛 , 𝑥 ⟩ ) ) )
52 28 51 vtocle ⊢ ( 𝑛 ∈ ω → ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) = ⟨ 𝑛 , 𝑥 ⟩ ) )
53 27 52 biimtrrid ⊢ ( 𝑛 ∈ ω → ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) = ⟨ 𝑛 , 𝑥 ⟩ ) )
54 53 anabsi5 ⊢ ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) = ⟨ 𝑛 , 𝑥 ⟩ )
55 vex ⊢ 𝑥 ∈ V
56 28 55 opnzi ⊢ ⟨ 𝑛 , 𝑥 ⟩ ≠ ∅
57 56 a1i ⊢ ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ) → ⟨ 𝑛 , 𝑥 ⟩ ≠ ∅ )
58 54 57 eqnetrd ⊢ ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ) → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) ≠ ∅ )
59 58 necomd ⊢ ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ) → ∅ ≠ ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) )
60 59 neneqd ⊢ ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑥 ∈ ( V × 𝑈 ) ) ) → ¬ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑥 ⟩ ) ‘ 𝑛 ) )
61 15 26 60 chvarfv ⊢ ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) ) → ¬ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) )
62 61 intnand ⊢ ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) ) → ¬ ( 𝑛 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) )
63 62 adantl ⊢ ( ( 𝑛 = 𝑁 ∧ ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) ) ) → ¬ ( 𝑛 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) )
64 opeq1 ⊢ ( 𝑛 = 𝑁 → ⟨ 𝑛 , 𝑦 ⟩ = ⟨ 𝑁 , 𝑦 ⟩ )
65 rdgeq2 ⊢ ( ⟨ 𝑛 , 𝑦 ⟩ = ⟨ 𝑁 , 𝑦 ⟩ → rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) = rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) )
66 64 65 syl ⊢ ( 𝑛 = 𝑁 → rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) = rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) )
67 id ⊢ ( 𝑛 = 𝑁 → 𝑛 = 𝑁 )
68 66 67 fveq12d ⊢ ( 𝑛 = 𝑁 → ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) )
69 68 eqeq2d ⊢ ( 𝑛 = 𝑁 → ( ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ↔ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) )
70 2 69 anbi12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) ↔ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) ) )
71 70 abbidv ⊢ ( 𝑛 = 𝑁 → { 𝑦 ∣ ( 𝑛 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) } = { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) } )
72 1 dffinxpf ⊢ ( 𝑈 ↑↑ 𝑁 ) = { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) }
73 71 72 eqtr4di ⊢ ( 𝑛 = 𝑁 → { 𝑦 ∣ ( 𝑛 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) } = ( 𝑈 ↑↑ 𝑁 ) )
74 73 eleq2d ⊢ ( 𝑛 = 𝑁 → ( 𝑦 ∈ { 𝑦 ∣ ( 𝑛 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) } ↔ 𝑦 ∈ ( 𝑈 ↑↑ 𝑁 ) ) )
75 abid ⊢ ( 𝑦 ∈ { 𝑦 ∣ ( 𝑛 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) } ↔ ( 𝑛 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) )
76 74 75 bitr3di ⊢ ( 𝑛 = 𝑁 → ( 𝑦 ∈ ( 𝑈 ↑↑ 𝑁 ) ↔ ( 𝑛 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) ) )
77 76 adantr ⊢ ( ( 𝑛 = 𝑁 ∧ ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) ) ) → ( 𝑦 ∈ ( 𝑈 ↑↑ 𝑁 ) ↔ ( 𝑛 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑛 , 𝑦 ⟩ ) ‘ 𝑛 ) ) ) )
78 63 77 mtbird ⊢ ( ( 𝑛 = 𝑁 ∧ ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) ) ) → ¬ 𝑦 ∈ ( 𝑈 ↑↑ 𝑁 ) )
79 78 ex ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ∈ ω ∧ ( 1o ∈ 𝑛 ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) ) → ¬ 𝑦 ∈ ( 𝑈 ↑↑ 𝑁 ) ) )
80 5 79 biimtrid ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ∧ ¬ 𝑦 ∈ ( V × 𝑈 ) ) → ¬ 𝑦 ∈ ( 𝑈 ↑↑ 𝑁 ) ) )
81 80 expdimp ⊢ ( ( 𝑛 = 𝑁 ∧ ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ) → ( ¬ 𝑦 ∈ ( V × 𝑈 ) → ¬ 𝑦 ∈ ( 𝑈 ↑↑ 𝑁 ) ) )
82 81 con4d ⊢ ( ( 𝑛 = 𝑁 ∧ ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ) → ( 𝑦 ∈ ( 𝑈 ↑↑ 𝑁 ) → 𝑦 ∈ ( V × 𝑈 ) ) )
83 82 ssrdv ⊢ ( ( 𝑛 = 𝑁 ∧ ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) ) → ( 𝑈 ↑↑ 𝑁 ) ⊆ ( V × 𝑈 ) )
84 83 ex ⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ∈ ω ∧ 1o ∈ 𝑛 ) → ( 𝑈 ↑↑ 𝑁 ) ⊆ ( V × 𝑈 ) ) )
85 4 84 sylbird ⊢ ( 𝑛 = 𝑁 → ( ( 𝑁 ∈ ω ∧ 1o ∈ 𝑁 ) → ( 𝑈 ↑↑ 𝑁 ) ⊆ ( V × 𝑈 ) ) )
86 85 vtocleg ⊢ ( 𝑁 ∈ ω → ( ( 𝑁 ∈ ω ∧ 1o ∈ 𝑁 ) → ( 𝑈 ↑↑ 𝑁 ) ⊆ ( V × 𝑈 ) ) )
87 86 anabsi5 ⊢ ( ( 𝑁 ∈ ω ∧ 1o ∈ 𝑁 ) → ( 𝑈 ↑↑ 𝑁 ) ⊆ ( V × 𝑈 ) )