Metamath Proof Explorer

Theorem fineqvnttrclselem3

Description: Lemma for fineqvnttrclse . (Contributed by BTernaryTau, 12-Jan-2026)

Ref Expression
Hypotheses fineqvnttrclselem3.1 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦 ) }
fineqvnttrclselem3.2 ⊢ 𝐴 = ω
fineqvnttrclselem3.3 ⊢ 𝐹 = ( 𝑣 ∈ suc suc 𝑁 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝐵 } )
Assertion fineqvnttrclselem3 ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ) → ∀ 𝑎 ∈ suc 𝑁 ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ suc 𝑎 ) )

Proof

Step Hyp Ref Expression
1 fineqvnttrclselem3.1 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦 ) }
2 fineqvnttrclselem3.2 ⊢ 𝐴 = ω
3 fineqvnttrclselem3.3 ⊢ 𝐹 = ( 𝑣 ∈ suc suc 𝑁 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝐵 } )
4 oveq1 ⊢ ( 𝑣 = 𝑎 → ( 𝑣 +o 𝑑 ) = ( 𝑎 +o 𝑑 ) )
5 4 eqeq1d ⊢ ( 𝑣 = 𝑎 → ( ( 𝑣 +o 𝑑 ) = 𝐵 ↔ ( 𝑎 +o 𝑑 ) = 𝐵 ) )
6 5 rabbidv ⊢ ( 𝑣 = 𝑎 → { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝐵 } = { 𝑑 ∈ On ∣ ( 𝑎 +o 𝑑 ) = 𝐵 } )
7 6 unieqd ⊢ ( 𝑣 = 𝑎 → ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝐵 } = ∪ { 𝑑 ∈ On ∣ ( 𝑎 +o 𝑑 ) = 𝐵 } )
8 elelsuc ⊢ ( 𝑎 ∈ suc 𝑁 → 𝑎 ∈ suc suc 𝑁 )
9 8 adantl ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑎 ∈ suc 𝑁 ) → 𝑎 ∈ suc suc 𝑁 )
10 fineqvnttrclselem1 ⊢ ( 𝐵 ∈ ( ω ∖ 1o ) → ∪ { 𝑑 ∈ On ∣ ( 𝑎 +o 𝑑 ) = 𝐵 } ∈ ω )
11 10 adantr ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑎 ∈ suc 𝑁 ) → ∪ { 𝑑 ∈ On ∣ ( 𝑎 +o 𝑑 ) = 𝐵 } ∈ ω )
12 3 7 9 11 fvmptd3 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑎 ∈ suc 𝑁 ) → ( 𝐹 ‘ 𝑎 ) = ∪ { 𝑑 ∈ On ∣ ( 𝑎 +o 𝑑 ) = 𝐵 } )
13 12 11 eqeltrd ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑎 ∈ suc 𝑁 ) → ( 𝐹 ‘ 𝑎 ) ∈ ω )
14 13 3adant2 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc 𝑁 ) → ( 𝐹 ‘ 𝑎 ) ∈ ω )
15 14 2 eleqtrrdi ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc 𝑁 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝐴 )
16 3 fineqvnttrclselem2 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc suc 𝑁 ) → ( 𝑎 +o ( 𝐹 ‘ 𝑎 ) ) = 𝐵 )
17 8 16 syl3an3 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc 𝑁 ) → ( 𝑎 +o ( 𝐹 ‘ 𝑎 ) ) = 𝐵 )
18 eldifi ⊢ ( 𝐵 ∈ ( ω ∖ 1o ) → 𝐵 ∈ ω )
19 elnn ⊢ ( ( 𝑁 ∈ 𝐵 ∧ 𝐵 ∈ ω ) → 𝑁 ∈ ω )
20 19 ancoms ⊢ ( ( 𝐵 ∈ ω ∧ 𝑁 ∈ 𝐵 ) → 𝑁 ∈ ω )
21 18 20 sylan ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ) → 𝑁 ∈ ω )
22 peano2 ⊢ ( 𝑁 ∈ ω → suc 𝑁 ∈ ω )
23 nnord ⊢ ( suc 𝑁 ∈ ω → Ord suc 𝑁 )
24 ordsucelsuc ⊢ ( Ord suc 𝑁 → ( 𝑎 ∈ suc 𝑁 ↔ suc 𝑎 ∈ suc suc 𝑁 ) )
25 22 23 24 3syl ⊢ ( 𝑁 ∈ ω → ( 𝑎 ∈ suc 𝑁 ↔ suc 𝑎 ∈ suc suc 𝑁 ) )
26 25 biimpa ⊢ ( ( 𝑁 ∈ ω ∧ 𝑎 ∈ suc 𝑁 ) → suc 𝑎 ∈ suc suc 𝑁 )
27 21 26 stoic3 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc 𝑁 ) → suc 𝑎 ∈ suc suc 𝑁 )
28 3 fineqvnttrclselem2 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ suc 𝑎 ∈ suc suc 𝑁 ) → ( suc 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) = 𝐵 )
29 27 28 syld3an3 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc 𝑁 ) → ( suc 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) = 𝐵 )
30 17 29 eqtr4d ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc 𝑁 ) → ( 𝑎 +o ( 𝐹 ‘ 𝑎 ) ) = ( suc 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) )
31 21 22 syl ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ) → suc 𝑁 ∈ ω )
32 elnn ⊢ ( ( 𝑎 ∈ suc 𝑁 ∧ suc 𝑁 ∈ ω ) → 𝑎 ∈ ω )
33 32 ancoms ⊢ ( ( suc 𝑁 ∈ ω ∧ 𝑎 ∈ suc 𝑁 ) → 𝑎 ∈ ω )
34 31 33 stoic3 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc 𝑁 ) → 𝑎 ∈ ω )
35 21 3adant3 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc 𝑁 ) → 𝑁 ∈ ω )
36 oveq1 ⊢ ( 𝑣 = suc 𝑎 → ( 𝑣 +o 𝑑 ) = ( suc 𝑎 +o 𝑑 ) )
37 36 eqeq1d ⊢ ( 𝑣 = suc 𝑎 → ( ( 𝑣 +o 𝑑 ) = 𝐵 ↔ ( suc 𝑎 +o 𝑑 ) = 𝐵 ) )
38 37 rabbidv ⊢ ( 𝑣 = suc 𝑎 → { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝐵 } = { 𝑑 ∈ On ∣ ( suc 𝑎 +o 𝑑 ) = 𝐵 } )
39 38 unieqd ⊢ ( 𝑣 = suc 𝑎 → ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝐵 } = ∪ { 𝑑 ∈ On ∣ ( suc 𝑎 +o 𝑑 ) = 𝐵 } )
40 26 3adant1 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ ω ∧ 𝑎 ∈ suc 𝑁 ) → suc 𝑎 ∈ suc suc 𝑁 )
41 fineqvnttrclselem1 ⊢ ( 𝐵 ∈ ( ω ∖ 1o ) → ∪ { 𝑑 ∈ On ∣ ( suc 𝑎 +o 𝑑 ) = 𝐵 } ∈ ω )
42 41 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ ω ∧ 𝑎 ∈ suc 𝑁 ) → ∪ { 𝑑 ∈ On ∣ ( suc 𝑎 +o 𝑑 ) = 𝐵 } ∈ ω )
43 3 39 40 42 fvmptd3 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ ω ∧ 𝑎 ∈ suc 𝑁 ) → ( 𝐹 ‘ suc 𝑎 ) = ∪ { 𝑑 ∈ On ∣ ( suc 𝑎 +o 𝑑 ) = 𝐵 } )
44 43 42 eqeltrd ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ ω ∧ 𝑎 ∈ suc 𝑁 ) → ( 𝐹 ‘ suc 𝑎 ) ∈ ω )
45 35 44 syld3an2 ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc 𝑁 ) → ( 𝐹 ‘ suc 𝑎 ) ∈ ω )
46 nnacom ⊢ ( ( 𝑎 ∈ ω ∧ ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → ( 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) = ( ( 𝐹 ‘ suc 𝑎 ) +o 𝑎 ) )
47 46 suceqd ⊢ ( ( 𝑎 ∈ ω ∧ ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → suc ( 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) = suc ( ( 𝐹 ‘ suc 𝑎 ) +o 𝑎 ) )
48 nnasuc ⊢ ( ( 𝑎 ∈ ω ∧ ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → ( 𝑎 +o suc ( 𝐹 ‘ suc 𝑎 ) ) = suc ( 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) )
49 nnasuc ⊢ ( ( ( 𝐹 ‘ suc 𝑎 ) ∈ ω ∧ 𝑎 ∈ ω ) → ( ( 𝐹 ‘ suc 𝑎 ) +o suc 𝑎 ) = suc ( ( 𝐹 ‘ suc 𝑎 ) +o 𝑎 ) )
50 49 ancoms ⊢ ( ( 𝑎 ∈ ω ∧ ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → ( ( 𝐹 ‘ suc 𝑎 ) +o suc 𝑎 ) = suc ( ( 𝐹 ‘ suc 𝑎 ) +o 𝑎 ) )
51 47 48 50 3eqtr4d ⊢ ( ( 𝑎 ∈ ω ∧ ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → ( 𝑎 +o suc ( 𝐹 ‘ suc 𝑎 ) ) = ( ( 𝐹 ‘ suc 𝑎 ) +o suc 𝑎 ) )
52 peano2 ⊢ ( 𝑎 ∈ ω → suc 𝑎 ∈ ω )
53 nnacom ⊢ ( ( suc 𝑎 ∈ ω ∧ ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → ( suc 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) = ( ( 𝐹 ‘ suc 𝑎 ) +o suc 𝑎 ) )
54 52 53 sylan ⊢ ( ( 𝑎 ∈ ω ∧ ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → ( suc 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) = ( ( 𝐹 ‘ suc 𝑎 ) +o suc 𝑎 ) )
55 51 54 eqtr4d ⊢ ( ( 𝑎 ∈ ω ∧ ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → ( 𝑎 +o suc ( 𝐹 ‘ suc 𝑎 ) ) = ( suc 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) )
56 55 3adant2 ⊢ ( ( 𝑎 ∈ ω ∧ ( 𝐹 ‘ 𝑎 ) ∈ ω ∧ ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → ( 𝑎 +o suc ( 𝐹 ‘ suc 𝑎 ) ) = ( suc 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) )
57 56 eqeq2d ⊢ ( ( 𝑎 ∈ ω ∧ ( 𝐹 ‘ 𝑎 ) ∈ ω ∧ ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → ( ( 𝑎 +o ( 𝐹 ‘ 𝑎 ) ) = ( 𝑎 +o suc ( 𝐹 ‘ suc 𝑎 ) ) ↔ ( 𝑎 +o ( 𝐹 ‘ 𝑎 ) ) = ( suc 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) ) )
58 peano2 ⊢ ( ( 𝐹 ‘ suc 𝑎 ) ∈ ω → suc ( 𝐹 ‘ suc 𝑎 ) ∈ ω )
59 nnacan ⊢ ( ( 𝑎 ∈ ω ∧ ( 𝐹 ‘ 𝑎 ) ∈ ω ∧ suc ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → ( ( 𝑎 +o ( 𝐹 ‘ 𝑎 ) ) = ( 𝑎 +o suc ( 𝐹 ‘ suc 𝑎 ) ) ↔ ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ suc 𝑎 ) ) )
60 58 59 syl3an3 ⊢ ( ( 𝑎 ∈ ω ∧ ( 𝐹 ‘ 𝑎 ) ∈ ω ∧ ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → ( ( 𝑎 +o ( 𝐹 ‘ 𝑎 ) ) = ( 𝑎 +o suc ( 𝐹 ‘ suc 𝑎 ) ) ↔ ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ suc 𝑎 ) ) )
61 57 60 bitr3d ⊢ ( ( 𝑎 ∈ ω ∧ ( 𝐹 ‘ 𝑎 ) ∈ ω ∧ ( 𝐹 ‘ suc 𝑎 ) ∈ ω ) → ( ( 𝑎 +o ( 𝐹 ‘ 𝑎 ) ) = ( suc 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) ↔ ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ suc 𝑎 ) ) )
62 34 14 45 61 syl3anc ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc 𝑁 ) → ( ( 𝑎 +o ( 𝐹 ‘ 𝑎 ) ) = ( suc 𝑎 +o ( 𝐹 ‘ suc 𝑎 ) ) ↔ ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ suc 𝑎 ) ) )
63 30 62 mpbid ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc 𝑁 ) → ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ suc 𝑎 ) )
64 fvex ⊢ ( 𝐹 ‘ 𝑎 ) ∈ V
65 fvex ⊢ ( 𝐹 ‘ suc 𝑎 ) ∈ V
66 eleq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( 𝑥 ∈ 𝐴 ↔ ( 𝐹 ‘ 𝑎 ) ∈ 𝐴 ) )
67 eqeq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( 𝑥 = suc 𝑦 ↔ ( 𝐹 ‘ 𝑎 ) = suc 𝑦 ) )
68 66 67 anbi12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 = suc 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑎 ) = suc 𝑦 ) ) )
69 suceq ⊢ ( 𝑦 = ( 𝐹 ‘ suc 𝑎 ) → suc 𝑦 = suc ( 𝐹 ‘ suc 𝑎 ) )
70 69 eqeq2d ⊢ ( 𝑦 = ( 𝐹 ‘ suc 𝑎 ) → ( ( 𝐹 ‘ 𝑎 ) = suc 𝑦 ↔ ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ suc 𝑎 ) ) )
71 70 anbi2d ⊢ ( 𝑦 = ( 𝐹 ‘ suc 𝑎 ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑎 ) = suc 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ suc 𝑎 ) ) ) )
72 64 65 68 71 1 brab ⊢ ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ suc 𝑎 ) ↔ ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑎 ) = suc ( 𝐹 ‘ suc 𝑎 ) ) )
73 15 63 72 sylanbrc ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝑎 ∈ suc 𝑁 ) → ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ suc 𝑎 ) )
74 73 3expia ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ) → ( 𝑎 ∈ suc 𝑁 → ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ suc 𝑎 ) ) )
75 74 ralrimiv ⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ) → ∀ 𝑎 ∈ suc 𝑁 ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ suc 𝑎 ) )