Metamath Proof Explorer

Theorem fineqvnttrclselem1

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

Ref Expression
Assertion fineqvnttrclselem1 ( 𝐵 ∈ ( ω ∖ 1o ) → ∪ { 𝑑 ∈ On ∣ ( 𝐴 +o 𝑑 ) = 𝐵 } ∈ ω )

Proof

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