Metamath Proof Explorer

Theorem fineqvnttrclselem2

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

Ref Expression
Hypothesis fineqvnttrclselem2.1 ⊢ F = v ∈ suc ⁡ suc ⁡ N ⟼ ⋃ d ∈ On | v + 𝑜 d = B
Assertion fineqvnttrclselem2 ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → A + 𝑜 F ⁡ A = B

Proof

Step Hyp Ref Expression
1 fineqvnttrclselem2.1 ⊢ F = v ∈ suc ⁡ suc ⁡ N ⟼ ⋃ d ∈ On | v + 𝑜 d = B
2 eldifi ⊢ B ∈ ω ∖ 1 𝑜 → B ∈ ω
3 elnn ⊢ N ∈ B ∧ B ∈ ω → N ∈ ω
4 3 ancoms ⊢ B ∈ ω ∧ N ∈ B → N ∈ ω
5 2 4 sylan ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B → N ∈ ω
6 5 3adant3 ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → N ∈ ω
7 oveq1 ⊢ v = A → v + 𝑜 d = A + 𝑜 d
8 7 eqeq1d ⊢ v = A → v + 𝑜 d = B ↔ A + 𝑜 d = B
9 8 rabbidv ⊢ v = A → d ∈ On | v + 𝑜 d = B = d ∈ On | A + 𝑜 d = B
10 9 unieqd ⊢ v = A → ⋃ d ∈ On | v + 𝑜 d = B = ⋃ d ∈ On | A + 𝑜 d = B
11 simp3 ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ ω ∧ A ∈ suc ⁡ suc ⁡ N → A ∈ suc ⁡ suc ⁡ N
12 fineqvnttrclselem1 ⊢ B ∈ ω ∖ 1 𝑜 → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω
13 12 3ad2ant1 ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ ω ∧ A ∈ suc ⁡ suc ⁡ N → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω
14 1 10 11 13 fvmptd3 ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ ω ∧ A ∈ suc ⁡ suc ⁡ N → F ⁡ A = ⋃ d ∈ On | A + 𝑜 d = B
15 6 14 syld3an2 ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → F ⁡ A = ⋃ d ∈ On | A + 𝑜 d = B
16 nnon ⊢ B ∈ ω → B ∈ On
17 2 16 syl ⊢ B ∈ ω ∖ 1 𝑜 → B ∈ On
18 onelon ⊢ B ∈ On ∧ N ∈ B → N ∈ On
19 onsuc ⊢ N ∈ On → suc ⁡ N ∈ On
20 18 19 syl ⊢ B ∈ On ∧ N ∈ B → suc ⁡ N ∈ On
21 17 20 sylan ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B → suc ⁡ N ∈ On
22 onsuc ⊢ suc ⁡ N ∈ On → suc ⁡ suc ⁡ N ∈ On
23 onelon ⊢ suc ⁡ suc ⁡ N ∈ On ∧ A ∈ suc ⁡ suc ⁡ N → A ∈ On
24 22 23 sylan ⊢ suc ⁡ N ∈ On ∧ A ∈ suc ⁡ suc ⁡ N → A ∈ On
25 21 24 stoic3 ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → A ∈ On
26 17 3ad2ant1 ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → B ∈ On
27 simp3 ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → A ∈ suc ⁡ suc ⁡ N
28 simpl ⊢ suc ⁡ N ∈ On ∧ A ∈ suc ⁡ suc ⁡ N → suc ⁡ N ∈ On
29 24 28 jca ⊢ suc ⁡ N ∈ On ∧ A ∈ suc ⁡ suc ⁡ N → A ∈ On ∧ suc ⁡ N ∈ On
30 21 29 stoic3 ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → A ∈ On ∧ suc ⁡ N ∈ On
31 onsssuc ⊢ A ∈ On ∧ suc ⁡ N ∈ On → A ⊆ suc ⁡ N ↔ A ∈ suc ⁡ suc ⁡ N
32 30 31 syl ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → A ⊆ suc ⁡ N ↔ A ∈ suc ⁡ suc ⁡ N
33 27 32 mpbird ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → A ⊆ suc ⁡ N
34 nnord ⊢ B ∈ ω → Ord ⁡ B
35 ordsucss ⊢ Ord ⁡ B → N ∈ B → suc ⁡ N ⊆ B
36 2 34 35 3syl ⊢ B ∈ ω ∖ 1 𝑜 → N ∈ B → suc ⁡ N ⊆ B
37 36 imp ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B → suc ⁡ N ⊆ B
38 37 3adant3 ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → suc ⁡ N ⊆ B
39 33 38 sstrd ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → A ⊆ B
40 oawordeu ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ B → ∃! d ∈ On A + 𝑜 d = B
41 25 26 39 40 syl21anc ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → ∃! d ∈ On A + 𝑜 d = B
42 reusn ⊢ ∃! d ∈ On A + 𝑜 d = B ↔ ∃ x d ∈ On | A + 𝑜 d = B = x
43 unieq ⊢ d ∈ On | A + 𝑜 d = B = x → ⋃ d ∈ On | A + 𝑜 d = B = ⋃ x
44 unisnv ⊢ ⋃ x = x
45 43 44 eqtrdi ⊢ d ∈ On | A + 𝑜 d = B = x → ⋃ d ∈ On | A + 𝑜 d = B = x
46 vsnid ⊢ x ∈ x
47 eleq2 ⊢ d ∈ On | A + 𝑜 d = B = x → x ∈ d ∈ On | A + 𝑜 d = B ↔ x ∈ x
48 46 47 mpbiri ⊢ d ∈ On | A + 𝑜 d = B = x → x ∈ d ∈ On | A + 𝑜 d = B
49 45 48 eqeltrd ⊢ d ∈ On | A + 𝑜 d = B = x → ⋃ d ∈ On | A + 𝑜 d = B ∈ d ∈ On | A + 𝑜 d = B
50 49 exlimiv ⊢ ∃ x d ∈ On | A + 𝑜 d = B = x → ⋃ d ∈ On | A + 𝑜 d = B ∈ d ∈ On | A + 𝑜 d = B
51 42 50 sylbi ⊢ ∃! d ∈ On A + 𝑜 d = B → ⋃ d ∈ On | A + 𝑜 d = B ∈ d ∈ On | A + 𝑜 d = B
52 41 51 syl ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → ⋃ d ∈ On | A + 𝑜 d = B ∈ d ∈ On | A + 𝑜 d = B
53 15 52 eqeltrd ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → F ⁡ A ∈ d ∈ On | A + 𝑜 d = B
54 oveq2 ⊢ d = F ⁡ A → A + 𝑜 d = A + 𝑜 F ⁡ A
55 54 eqeq1d ⊢ d = F ⁡ A → A + 𝑜 d = B ↔ A + 𝑜 F ⁡ A = B
56 55 elrab ⊢ F ⁡ A ∈ d ∈ On | A + 𝑜 d = B ↔ F ⁡ A ∈ On ∧ A + 𝑜 F ⁡ A = B
57 53 56 sylib ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → F ⁡ A ∈ On ∧ A + 𝑜 F ⁡ A = B
58 57 simprd ⊢ B ∈ ω ∖ 1 𝑜 ∧ N ∈ B ∧ A ∈ suc ⁡ suc ⁡ N → A + 𝑜 F ⁡ A = B