Metamath Proof Explorer

Theorem fineqvnttrclselem1

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

Ref Expression
Assertion fineqvnttrclselem1 
|- ( B e. ( _om \ 1o ) -> U. { d e. On | ( A +o d ) = B } e. _om )

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( B e. ( _om \ 1o ) -> B e. _om )
2 eleq1 
 |-  ( ( A +o d ) = B -> ( ( A +o d ) e. _om <-> B e. _om ) )
3 2 biimparc 
 |-  ( ( B e. _om /\ ( A +o d ) = B ) -> ( A +o d ) e. _om )
4 3 adantll 
 |-  ( ( ( A e. On /\ B e. _om ) /\ ( A +o d ) = B ) -> ( A +o d ) e. _om )
5 4 3adant2 
 |-  ( ( ( A e. On /\ B e. _om ) /\ d e. On /\ ( A +o d ) = B ) -> ( A +o d ) e. _om )
6 nnarcl 
 |-  ( ( A e. On /\ d e. On ) -> ( ( A +o d ) e. _om <-> ( A e. _om /\ d e. _om ) ) )
7 6 adantlr 
 |-  ( ( ( A e. On /\ B e. _om ) /\ d e. On ) -> ( ( A +o d ) e. _om <-> ( A e. _om /\ d e. _om ) ) )
8 7 3adant3 
 |-  ( ( ( A e. On /\ B e. _om ) /\ d e. On /\ ( A +o d ) = B ) -> ( ( A +o d ) e. _om <-> ( A e. _om /\ d e. _om ) ) )
9 5 8 mpbid 
 |-  ( ( ( A e. On /\ B e. _om ) /\ d e. On /\ ( A +o d ) = B ) -> ( A e. _om /\ d e. _om ) )
10 9 simprd 
 |-  ( ( ( A e. On /\ B e. _om ) /\ d e. On /\ ( A +o d ) = B ) -> d e. _om )
11 10 rabssdv 
 |-  ( ( A e. On /\ B e. _om ) -> { d e. On | ( A +o d ) = B } C_ _om )
12 nnon 
 |-  ( B e. _om -> B e. On )
13 oawordeu 
 |-  ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> E! d e. On ( A +o d ) = B )
14 reusn 
 |-  ( E! d e. On ( A +o d ) = B <-> E. w { d e. On | ( A +o d ) = B } = { w } )
15 snfi 
 |-  { w } e. Fin
16 eleq1 
 |-  ( { d e. On | ( A +o d ) = B } = { w } -> ( { d e. On | ( A +o d ) = B } e. Fin <-> { w } e. Fin ) )
17 15 16 mpbiri 
 |-  ( { d e. On | ( A +o d ) = B } = { w } -> { d e. On | ( A +o d ) = B } e. Fin )
18 17 exlimiv 
 |-  ( E. w { d e. On | ( A +o d ) = B } = { w } -> { d e. On | ( A +o d ) = B } e. Fin )
19 14 18 sylbi 
 |-  ( E! d e. On ( A +o d ) = B -> { d e. On | ( A +o d ) = B } e. Fin )
20 13 19 syl 
 |-  ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> { d e. On | ( A +o d ) = B } e. Fin )
21 12 20 sylanl2 
 |-  ( ( ( A e. On /\ B e. _om ) /\ A C_ B ) -> { d e. On | ( A +o d ) = B } e. Fin )
22 nnunifi 
 |-  ( ( { d e. On | ( A +o d ) = B } C_ _om /\ { d e. On | ( A +o d ) = B } e. Fin ) -> U. { d e. On | ( A +o d ) = B } e. _om )
23 11 21 22 syl2an2r 
 |-  ( ( ( A e. On /\ B e. _om ) /\ A C_ B ) -> U. { d e. On | ( A +o d ) = B } e. _om )
24 oawordex 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> E. d e. On ( A +o d ) = B ) )
25 12 24 sylan2 
 |-  ( ( A e. On /\ B e. _om ) -> ( A C_ B <-> E. d e. On ( A +o d ) = B ) )
26 25 notbid 
 |-  ( ( A e. On /\ B e. _om ) -> ( -. A C_ B <-> -. E. d e. On ( A +o d ) = B ) )
27 26 biimpa 
 |-  ( ( ( A e. On /\ B e. _om ) /\ -. A C_ B ) -> -. E. d e. On ( A +o d ) = B )
28 ralnex 
 |-  ( A. d e. On -. ( A +o d ) = B <-> -. E. d e. On ( A +o d ) = B )
29 rabeq0 
 |-  ( { d e. On | ( A +o d ) = B } = (/) <-> A. d e. On -. ( A +o d ) = B )
30 29 biimpri 
 |-  ( A. d e. On -. ( A +o d ) = B -> { d e. On | ( A +o d ) = B } = (/) )
31 30 unieqd 
 |-  ( A. d e. On -. ( A +o d ) = B -> U. { d e. On | ( A +o d ) = B } = U. (/) )
32 uni0 
 |-  U. (/) = (/)
33 31 32 eqtrdi 
 |-  ( A. d e. On -. ( A +o d ) = B -> U. { d e. On | ( A +o d ) = B } = (/) )
34 peano1 
 |-  (/) e. _om
35 33 34 eqeltrdi 
 |-  ( A. d e. On -. ( A +o d ) = B -> U. { d e. On | ( A +o d ) = B } e. _om )
36 28 35 sylbir 
 |-  ( -. E. d e. On ( A +o d ) = B -> U. { d e. On | ( A +o d ) = B } e. _om )
37 27 36 syl 
 |-  ( ( ( A e. On /\ B e. _om ) /\ -. A C_ B ) -> U. { d e. On | ( A +o d ) = B } e. _om )
38 23 37 pm2.61dan 
 |-  ( ( A e. On /\ B e. _om ) -> U. { d e. On | ( A +o d ) = B } e. _om )
39 38 expcom 
 |-  ( B e. _om -> ( A e. On -> U. { d e. On | ( A +o d ) = B } e. _om ) )
40 1 39 syl 
 |-  ( B e. ( _om \ 1o ) -> ( A e. On -> U. { d e. On | ( A +o d ) = B } e. _om ) )
41 simpl 
 |-  ( ( A e. On /\ d e. On ) -> A e. On )
42 df-oadd 
 |-  +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
43 42 mpondm0 
 |-  ( -. ( A e. On /\ d e. On ) -> ( A +o d ) = (/) )
44 41 43 nsyl5 
 |-  ( -. A e. On -> ( A +o d ) = (/) )
45 eldifsnneq 
 |-  ( B e. ( _om \ { (/) } ) -> -. B = (/) )
46 df1o2 
 |-  1o = { (/) }
47 46 difeq2i 
 |-  ( _om \ 1o ) = ( _om \ { (/) } )
48 45 47 eleq2s 
 |-  ( B e. ( _om \ 1o ) -> -. B = (/) )
49 eqtr2 
 |-  ( ( ( A +o d ) = B /\ ( A +o d ) = (/) ) -> B = (/) )
50 49 stoic1b 
 |-  ( ( ( A +o d ) = (/) /\ -. B = (/) ) -> -. ( A +o d ) = B )
51 44 48 50 syl2anr 
 |-  ( ( B e. ( _om \ 1o ) /\ -. A e. On ) -> -. ( A +o d ) = B )
52 51 ralrimivw 
 |-  ( ( B e. ( _om \ 1o ) /\ -. A e. On ) -> A. d e. On -. ( A +o d ) = B )
53 52 35 syl 
 |-  ( ( B e. ( _om \ 1o ) /\ -. A e. On ) -> U. { d e. On | ( A +o d ) = B } e. _om )
54 53 ex 
 |-  ( B e. ( _om \ 1o ) -> ( -. A e. On -> U. { d e. On | ( A +o d ) = B } e. _om ) )
55 40 54 pm2.61d 
 |-  ( B e. ( _om \ 1o ) -> U. { d e. On | ( A +o d ) = B } e. _om )