Metamath Proof Explorer

Theorem fineqvnttrclselem1

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

Ref Expression
Assertion fineqvnttrclselem1 ⊢ B ∈ ω ∖ 1 𝑜 → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω

Proof

Step Hyp Ref Expression
1 eldifi ⊢ B ∈ ω ∖ 1 𝑜 → B ∈ ω
2 eleq1 ⊢ A + 𝑜 d = B → A + 𝑜 d ∈ ω ↔ B ∈ ω
3 2 biimparc ⊢ B ∈ ω ∧ A + 𝑜 d = B → A + 𝑜 d ∈ ω
4 3 adantll ⊢ A ∈ On ∧ B ∈ ω ∧ A + 𝑜 d = B → A + 𝑜 d ∈ ω
5 4 3adant2 ⊢ A ∈ On ∧ B ∈ ω ∧ d ∈ On ∧ A + 𝑜 d = B → A + 𝑜 d ∈ ω
6 nnarcl ⊢ A ∈ On ∧ d ∈ On → A + 𝑜 d ∈ ω ↔ A ∈ ω ∧ d ∈ ω
7 6 adantlr ⊢ A ∈ On ∧ B ∈ ω ∧ d ∈ On → A + 𝑜 d ∈ ω ↔ A ∈ ω ∧ d ∈ ω
8 7 3adant3 ⊢ A ∈ On ∧ B ∈ ω ∧ d ∈ On ∧ A + 𝑜 d = B → A + 𝑜 d ∈ ω ↔ A ∈ ω ∧ d ∈ ω
9 5 8 mpbid ⊢ A ∈ On ∧ B ∈ ω ∧ d ∈ On ∧ A + 𝑜 d = B → A ∈ ω ∧ d ∈ ω
10 9 simprd ⊢ A ∈ On ∧ B ∈ ω ∧ d ∈ On ∧ A + 𝑜 d = B → d ∈ ω
11 10 rabssdv ⊢ A ∈ On ∧ B ∈ ω → d ∈ On | A + 𝑜 d = B ⊆ ω
12 nnon ⊢ B ∈ ω → B ∈ On
13 oawordeu ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ B → ∃! d ∈ On A + 𝑜 d = B
14 reusn ⊢ ∃! d ∈ On A + 𝑜 d = B ↔ ∃ w d ∈ On | A + 𝑜 d = B = w
15 snfi ⊢ w ∈ Fin
16 eleq1 ⊢ d ∈ On | A + 𝑜 d = B = w → d ∈ On | A + 𝑜 d = B ∈ Fin ↔ w ∈ Fin
17 15 16 mpbiri ⊢ d ∈ On | A + 𝑜 d = B = w → d ∈ On | A + 𝑜 d = B ∈ Fin
18 17 exlimiv ⊢ ∃ w d ∈ On | A + 𝑜 d = B = w → d ∈ On | A + 𝑜 d = B ∈ Fin
19 14 18 sylbi ⊢ ∃! d ∈ On A + 𝑜 d = B → d ∈ On | A + 𝑜 d = B ∈ Fin
20 13 19 syl ⊢ A ∈ On ∧ B ∈ On ∧ A ⊆ B → d ∈ On | A + 𝑜 d = B ∈ Fin
21 12 20 sylanl2 ⊢ A ∈ On ∧ B ∈ ω ∧ A ⊆ B → d ∈ On | A + 𝑜 d = B ∈ Fin
22 nnunifi ⊢ d ∈ On | A + 𝑜 d = B ⊆ ω ∧ d ∈ On | A + 𝑜 d = B ∈ Fin → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω
23 11 21 22 syl2an2r ⊢ A ∈ On ∧ B ∈ ω ∧ A ⊆ B → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω
24 oawordex ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ ∃ d ∈ On A + 𝑜 d = B
25 12 24 sylan2 ⊢ A ∈ On ∧ B ∈ ω → A ⊆ B ↔ ∃ d ∈ On A + 𝑜 d = B
26 25 notbid ⊢ A ∈ On ∧ B ∈ ω → ¬ A ⊆ B ↔ ¬ ∃ d ∈ On A + 𝑜 d = B
27 26 biimpa ⊢ A ∈ On ∧ B ∈ ω ∧ ¬ A ⊆ B → ¬ ∃ d ∈ On A + 𝑜 d = B
28 ralnex ⊢ ∀ d ∈ On ¬ A + 𝑜 d = B ↔ ¬ ∃ d ∈ On A + 𝑜 d = B
29 rabeq0 ⊢ d ∈ On | A + 𝑜 d = B = ∅ ↔ ∀ d ∈ On ¬ A + 𝑜 d = B
30 29 biimpri ⊢ ∀ d ∈ On ¬ A + 𝑜 d = B → d ∈ On | A + 𝑜 d = B = ∅
31 30 unieqd ⊢ ∀ d ∈ On ¬ A + 𝑜 d = B → ⋃ d ∈ On | A + 𝑜 d = B = ⋃ ∅
32 uni0 ⊢ ⋃ ∅ = ∅
33 31 32 eqtrdi ⊢ ∀ d ∈ On ¬ A + 𝑜 d = B → ⋃ d ∈ On | A + 𝑜 d = B = ∅
34 peano1 ⊢ ∅ ∈ ω
35 33 34 eqeltrdi ⊢ ∀ d ∈ On ¬ A + 𝑜 d = B → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω
36 28 35 sylbir ⊢ ¬ ∃ d ∈ On A + 𝑜 d = B → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω
37 27 36 syl ⊢ A ∈ On ∧ B ∈ ω ∧ ¬ A ⊆ B → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω
38 23 37 pm2.61dan ⊢ A ∈ On ∧ B ∈ ω → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω
39 38 expcom ⊢ B ∈ ω → A ∈ On → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω
40 1 39 syl ⊢ B ∈ ω ∖ 1 𝑜 → A ∈ On → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω
41 simpl ⊢ A ∈ On ∧ d ∈ On → A ∈ On
42 df-oadd ⊢ + 𝑜 = x ∈ On , y ∈ On ⟼ rec ⁡ z ∈ V ⟼ suc ⁡ z x ⁡ y
43 42 mpondm0 ⊢ ¬ A ∈ On ∧ d ∈ On → A + 𝑜 d = ∅
44 41 43 nsyl5 ⊢ ¬ A ∈ On → A + 𝑜 d = ∅
45 eldifsnneq ⊢ B ∈ ω ∖ ∅ → ¬ B = ∅
46 df1o2 ⊢ 1 𝑜 = ∅
47 46 difeq2i ⊢ ω ∖ 1 𝑜 = ω ∖ ∅
48 45 47 eleq2s ⊢ B ∈ ω ∖ 1 𝑜 → ¬ B = ∅
49 eqtr2 ⊢ A + 𝑜 d = B ∧ A + 𝑜 d = ∅ → B = ∅
50 49 stoic1b ⊢ A + 𝑜 d = ∅ ∧ ¬ B = ∅ → ¬ A + 𝑜 d = B
51 44 48 50 syl2anr ⊢ B ∈ ω ∖ 1 𝑜 ∧ ¬ A ∈ On → ¬ A + 𝑜 d = B
52 51 ralrimivw ⊢ B ∈ ω ∖ 1 𝑜 ∧ ¬ A ∈ On → ∀ d ∈ On ¬ A + 𝑜 d = B
53 52 35 syl ⊢ B ∈ ω ∖ 1 𝑜 ∧ ¬ A ∈ On → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω
54 53 ex ⊢ B ∈ ω ∖ 1 𝑜 → ¬ A ∈ On → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω
55 40 54 pm2.61d ⊢ B ∈ ω ∖ 1 𝑜 → ⋃ d ∈ On | A + 𝑜 d = B ∈ ω