Theorem nosupbnd1lem1

Description: Lemma for nosupbnd1 . Establish a soft upper bound. (Contributed by Scott Fenton, 5-Dec-2021)

	Ref	Expression
Hypothesis	nosupbnd1.1	⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
Assertion	nosupbnd1lem1	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ¬ 𝑆 <s ( 𝑈 ↾ dom 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		nosupbnd1.1	⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2		simp2l	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → 𝐴 ⊆ No )
3		simp3	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → 𝑈 ∈ 𝐴 )
4	2 3	sseldd	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → 𝑈 ∈ No )
5	1	nosupno	⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
6	5	3ad2ant2	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → 𝑆 ∈ No )
7		nodmon	⊢ ( 𝑆 ∈ No → dom 𝑆 ∈ On )
8	6 7	syl	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → dom 𝑆 ∈ On )
9		noreson	⊢ ( ( 𝑈 ∈ No ∧ dom 𝑆 ∈ On ) → ( 𝑈 ↾ dom 𝑆 ) ∈ No )
10	4 8 9	syl2anc	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ( 𝑈 ↾ dom 𝑆 ) ∈ No )
11		dmres	⊢ dom ( 𝑈 ↾ dom 𝑆 ) = ( dom 𝑆 ∩ dom 𝑈 )
12		inss1	⊢ ( dom 𝑆 ∩ dom 𝑈 ) ⊆ dom 𝑆
13	11 12	eqsstri	⊢ dom ( 𝑈 ↾ dom 𝑆 ) ⊆ dom 𝑆
14	13	a1i	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → dom ( 𝑈 ↾ dom 𝑆 ) ⊆ dom 𝑆 )
15		ssidd	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → dom 𝑆 ⊆ dom 𝑆 )
16		iffalse	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
17	1 16	eqtrid	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
18	17	dmeqd	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
19		iotaex	⊢ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ∈ V
20		eqid	⊢ ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) )
21	19 20	dmmpti	⊢ dom ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) = { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) }
22	18 21	eqtrdi	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } )
23	22	eleq2d	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ( ℎ ∈ dom 𝑆 ↔ ℎ ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ) )
24		vex	⊢ ℎ ∈ V
25		eleq1w	⊢ ( 𝑦 = ℎ → ( 𝑦 ∈ dom 𝑢 ↔ ℎ ∈ dom 𝑢 ) )
26		suceq	⊢ ( 𝑦 = ℎ → suc 𝑦 = suc ℎ )
27	26	reseq2d	⊢ ( 𝑦 = ℎ → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑢 ↾ suc ℎ ) )
28	26	reseq2d	⊢ ( 𝑦 = ℎ → ( 𝑣 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc ℎ ) )
29	27 28	eqeq12d	⊢ ( 𝑦 = ℎ → ( ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ↔ ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) )
30	29	imbi2d	⊢ ( 𝑦 = ℎ → ( ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) )
31	30	ralbidv	⊢ ( 𝑦 = ℎ → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) )
32	25 31	anbi12d	⊢ ( 𝑦 = ℎ → ( ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ( ℎ ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) )
33	32	rexbidv	⊢ ( 𝑦 = ℎ → ( ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑢 ∈ 𝐴 ( ℎ ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) )
34		dmeq	⊢ ( 𝑢 = 𝑝 → dom 𝑢 = dom 𝑝 )
35	34	eleq2d	⊢ ( 𝑢 = 𝑝 → ( ℎ ∈ dom 𝑢 ↔ ℎ ∈ dom 𝑝 ) )
36		breq2	⊢ ( 𝑢 = 𝑝 → ( 𝑣 <s 𝑢 ↔ 𝑣 <s 𝑝 ) )
37	36	notbid	⊢ ( 𝑢 = 𝑝 → ( ¬ 𝑣 <s 𝑢 ↔ ¬ 𝑣 <s 𝑝 ) )
38		reseq1	⊢ ( 𝑢 = 𝑝 → ( 𝑢 ↾ suc ℎ ) = ( 𝑝 ↾ suc ℎ ) )
39	38	eqeq1d	⊢ ( 𝑢 = 𝑝 → ( ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ↔ ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) )
40	37 39	imbi12d	⊢ ( 𝑢 = 𝑝 → ( ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ↔ ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) )
41	40	ralbidv	⊢ ( 𝑢 = 𝑝 → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ↔ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) )
42	35 41	anbi12d	⊢ ( 𝑢 = 𝑝 → ( ( ℎ ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ↔ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) )
43	42	cbvrexvw	⊢ ( ∃ 𝑢 ∈ 𝐴 ( ℎ ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) )
44	33 43	bitrdi	⊢ ( 𝑦 = ℎ → ( ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) )
45	24 44	elab	⊢ ( ℎ ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↔ ∃ 𝑝 ∈ 𝐴 ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) )
46	23 45	bitrdi	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ( ℎ ∈ dom 𝑆 ↔ ∃ 𝑝 ∈ 𝐴 ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) )
47	46	3ad2ant1	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ( ℎ ∈ dom 𝑆 ↔ ∃ 𝑝 ∈ 𝐴 ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) )
48		simpl1	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
49		simpl2	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
50		simprl	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → 𝑝 ∈ 𝐴 )
51		simprrl	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ℎ ∈ dom 𝑝 )
52		simprrr	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) )
53	1	nosupres	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑝 ∈ 𝐴 ∧ ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) → ( 𝑆 ↾ suc ℎ ) = ( 𝑝 ↾ suc ℎ ) )
54	48 49 50 51 52 53	syl113anc	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( 𝑆 ↾ suc ℎ ) = ( 𝑝 ↾ suc ℎ ) )
55		simpl2l	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → 𝐴 ⊆ No )
56	55 50	sseldd	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → 𝑝 ∈ No )
57	4	adantr	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → 𝑈 ∈ No )
58		sltso	⊢ <s Or No
59		soasym	⊢ ( ( <s Or No ∧ ( 𝑝 ∈ No ∧ 𝑈 ∈ No ) ) → ( 𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝 ) )
60	58 59	mpan	⊢ ( ( 𝑝 ∈ No ∧ 𝑈 ∈ No ) → ( 𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝 ) )
61	56 57 60	syl2anc	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( 𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝 ) )
62		simpl3	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → 𝑈 ∈ 𝐴 )
63		breq1	⊢ ( 𝑣 = 𝑈 → ( 𝑣 <s 𝑝 ↔ 𝑈 <s 𝑝 ) )
64	63	notbid	⊢ ( 𝑣 = 𝑈 → ( ¬ 𝑣 <s 𝑝 ↔ ¬ 𝑈 <s 𝑝 ) )
65		reseq1	⊢ ( 𝑣 = 𝑈 → ( 𝑣 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) )
66	65	eqeq2d	⊢ ( 𝑣 = 𝑈 → ( ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ↔ ( 𝑝 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) ) )
67	64 66	imbi12d	⊢ ( 𝑣 = 𝑈 → ( ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ↔ ( ¬ 𝑈 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) ) ) )
68	67	rspcv	⊢ ( 𝑈 ∈ 𝐴 → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) → ( ¬ 𝑈 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) ) ) )
69	62 52 68	sylc	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( ¬ 𝑈 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) ) )
70	61 69	syld	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( 𝑝 <s 𝑈 → ( 𝑝 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) ) )
71	70	imp	⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) ∧ 𝑝 <s 𝑈 ) → ( 𝑝 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) )
72		nodmon	⊢ ( 𝑝 ∈ No → dom 𝑝 ∈ On )
73	56 72	syl	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → dom 𝑝 ∈ On )
74		onelon	⊢ ( ( dom 𝑝 ∈ On ∧ ℎ ∈ dom 𝑝 ) → ℎ ∈ On )
75	73 51 74	syl2anc	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ℎ ∈ On )
76		onsucb	⊢ ( ℎ ∈ On ↔ suc ℎ ∈ On )
77	75 76	sylib	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → suc ℎ ∈ On )
78		noreson	⊢ ( ( 𝑈 ∈ No ∧ suc ℎ ∈ On ) → ( 𝑈 ↾ suc ℎ ) ∈ No )
79	57 77 78	syl2anc	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( 𝑈 ↾ suc ℎ ) ∈ No )
80		sonr	⊢ ( ( <s Or No ∧ ( 𝑈 ↾ suc ℎ ) ∈ No ) → ¬ ( 𝑈 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
81	58 80	mpan	⊢ ( ( 𝑈 ↾ suc ℎ ) ∈ No → ¬ ( 𝑈 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
82	79 81	syl	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ¬ ( 𝑈 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
83	82	adantr	⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) ∧ 𝑝 <s 𝑈 ) → ¬ ( 𝑈 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
84	71 83	eqnbrtrd	⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) ∧ 𝑝 <s 𝑈 ) → ¬ ( 𝑝 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
85	84	ex	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( 𝑝 <s 𝑈 → ¬ ( 𝑝 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) ) )
86		sltres	⊢ ( ( 𝑝 ∈ No ∧ 𝑈 ∈ No ∧ suc ℎ ∈ On ) → ( ( 𝑝 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) → 𝑝 <s 𝑈 ) )
87	56 57 77 86	syl3anc	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( ( 𝑝 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) → 𝑝 <s 𝑈 ) )
88	87	con3d	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( ¬ 𝑝 <s 𝑈 → ¬ ( 𝑝 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) ) )
89	85 88	pm2.61d	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ¬ ( 𝑝 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
90	54 89	eqnbrtrd	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ¬ ( 𝑆 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
91	90	rexlimdvaa	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ( ∃ 𝑝 ∈ 𝐴 ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) → ¬ ( 𝑆 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) ) )
92	47 91	sylbid	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ( ℎ ∈ dom 𝑆 → ¬ ( 𝑆 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) ) )
93	92	imp	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ℎ ∈ dom 𝑆 ) → ¬ ( 𝑆 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
94		nodmord	⊢ ( 𝑆 ∈ No → Ord dom 𝑆 )
95		ordsucss	⊢ ( Ord dom 𝑆 → ( ℎ ∈ dom 𝑆 → suc ℎ ⊆ dom 𝑆 ) )
96	6 94 95	3syl	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ( ℎ ∈ dom 𝑆 → suc ℎ ⊆ dom 𝑆 ) )
97	96	imp	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ℎ ∈ dom 𝑆 ) → suc ℎ ⊆ dom 𝑆 )
98	97	resabs1d	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ℎ ∈ dom 𝑆 ) → ( ( 𝑈 ↾ dom 𝑆 ) ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) )
99	98	breq2d	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ℎ ∈ dom 𝑆 ) → ( ( 𝑆 ↾ suc ℎ ) <s ( ( 𝑈 ↾ dom 𝑆 ) ↾ suc ℎ ) ↔ ( 𝑆 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) ) )
100	93 99	mtbird	⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ℎ ∈ dom 𝑆 ) → ¬ ( 𝑆 ↾ suc ℎ ) <s ( ( 𝑈 ↾ dom 𝑆 ) ↾ suc ℎ ) )
101	100	ralrimiva	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ∀ ℎ ∈ dom 𝑆 ¬ ( 𝑆 ↾ suc ℎ ) <s ( ( 𝑈 ↾ dom 𝑆 ) ↾ suc ℎ ) )
102		noresle	⊢ ( ( ( ( 𝑈 ↾ dom 𝑆 ) ∈ No ∧ 𝑆 ∈ No ) ∧ ( dom ( 𝑈 ↾ dom 𝑆 ) ⊆ dom 𝑆 ∧ dom 𝑆 ⊆ dom 𝑆 ∧ ∀ ℎ ∈ dom 𝑆 ¬ ( 𝑆 ↾ suc ℎ ) <s ( ( 𝑈 ↾ dom 𝑆 ) ↾ suc ℎ ) ) ) → ¬ 𝑆 <s ( 𝑈 ↾ dom 𝑆 ) )
103	10 6 14 15 101 102	syl23anc	⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ¬ 𝑆 <s ( 𝑈 ↾ dom 𝑆 ) )