Theorem fineqvnttrclselem2

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

	Ref	Expression
Hypothesis	fineqvnttrclselem2.1	⊢ 𝐹 = ( 𝑣 ∈ suc suc 𝑁 ↦ ∪ { 𝑑 ∈ On ∣ ( 𝑣 +o 𝑑 ) = 𝐵 } )
Assertion	fineqvnttrclselem2	⊢ ( ( 𝐵 ∈ ( ω ∖ 1o ) ∧ 𝑁 ∈ 𝐵 ∧ 𝐴 ∈ suc suc 𝑁 ) → ( 𝐴 +o ( 𝐹 ‘ 𝐴 ) ) = 𝐵 )

Proof

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