Theorem fineqvnttrclselem2

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

	Ref	Expression
Hypothesis	fineqvnttrclselem2.1	|- F = ( v e. suc suc N |-> U. { d e. On | ( v +o d ) = B } )
Assertion	fineqvnttrclselem2	|- ( ( B e. ( _om \ 1o ) /\ N e. B /\ A e. suc suc N ) -> ( A +o ( F ` A ) ) = B )

Proof

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