nosupbnd1lem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > nosupbnd1lem1		Structured version Visualization version GIF version

Theorem nosupbnd1lem1 27557

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

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

**Assertion**
Ref	Expression
nosupbnd1lem1	⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → ¬ 𝑆 <s (𝑈 ↾ dom 𝑆))

Distinct variable groups: 𝐴,𝑔,𝑢,𝑣,𝑥,𝑦 𝑣,𝑈 𝑥,𝑢,𝑦,𝑣 Allowed substitution hints: 𝑆(𝑥,𝑦,𝑣,𝑢,𝑔) 𝑈(𝑥,𝑦,𝑢,𝑔)

Proof of Theorem nosupbnd1lem1 Dummy variables ℎ 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp2l 1196	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → 𝐴 ⊆ No )
2		simp3 1135	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → 𝑈 ∈ 𝐴)
3	1, 2	sseldd 3975	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → 𝑈 ∈ No )
4		nosupbnd1.1	. . . . . 6 ⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
5	4	nosupno 27552	. . . . 5 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → 𝑆 ∈ No )
6	5	3ad2ant2 1131	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → 𝑆 ∈ No )
7		nodmon 27499	. . . 4 ⊢ (𝑆 ∈ No → dom 𝑆 ∈ On)
8	6, 7	syl 17	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → dom 𝑆 ∈ On)
9		noreson 27509	. . 3 ⊢ ((𝑈 ∈ No ∧ dom 𝑆 ∈ On) → (𝑈 ↾ dom 𝑆) ∈ No )
10	3, 8, 9	syl2anc 583	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → (𝑈 ↾ dom 𝑆) ∈ No )
11		dmres 5993	. . . 4 ⊢ dom (𝑈 ↾ dom 𝑆) = (dom 𝑆 ∩ dom 𝑈)
12		inss1 4220	. . . 4 ⊢ (dom 𝑆 ∩ dom 𝑈) ⊆ dom 𝑆
13	11, 12	eqsstri 4008	. . 3 ⊢ dom (𝑈 ↾ dom 𝑆) ⊆ dom 𝑆
14	13	a1i 11	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → dom (𝑈 ↾ dom 𝑆) ⊆ dom 𝑆)
15		ssidd 3997	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → dom 𝑆 ⊆ dom 𝑆)
16		iffalse 4529	. . . . . . . . . . . 12 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
17	4, 16	eqtrid 2776	. . . . . . . . . . 11 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
18	17	dmeqd 5895	. . . . . . . . . 10 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
19		iotaex 6506	. . . . . . . . . . 11 ⊢ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) ∈ V
20		eqid 2724	. . . . . . . . . . 11 ⊢ (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
21	19, 20	dmmpti 6684	. . . . . . . . . 10 ⊢ dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
22	18, 21	eqtrdi 2780	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
23	22	eleq2d 2811	. . . . . . . 8 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → (ℎ ∈ dom 𝑆 ↔ ℎ ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
24		vex 3470	. . . . . . . . 9 ⊢ ℎ ∈ V
25		eleq1w 2808	. . . . . . . . . . . 12 ⊢ (𝑦 = ℎ → (𝑦 ∈ dom 𝑢 ↔ ℎ ∈ dom 𝑢))
26		suceq 6420	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = ℎ → suc 𝑦 = suc ℎ)
27	26	reseq2d 5971	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ℎ → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc ℎ))
28	26	reseq2d 5971	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ℎ → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc ℎ))
29	27, 28	eqeq12d 2740	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ℎ → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))
30	29	imbi2d 340	. . . . . . . . . . . . 13 ⊢ (𝑦 = ℎ → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))
31	30	ralbidv 3169	. . . . . . . . . . . 12 ⊢ (𝑦 = ℎ → (∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))
32	25, 31	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑦 = ℎ → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (ℎ ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))))
33	32	rexbidv 3170	. . . . . . . . . 10 ⊢ (𝑦 = ℎ → (∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢 ∈ 𝐴 (ℎ ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))))
34		dmeq 5893	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
35	34	eleq2d 2811	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑝 → (ℎ ∈ dom 𝑢 ↔ ℎ ∈ dom 𝑝))
36		breq2 5142	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑝 → (𝑣 <s 𝑢 ↔ 𝑣 <s 𝑝))
37	36	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑝 → (¬ 𝑣 <s 𝑢 ↔ ¬ 𝑣 <s 𝑝))
38		reseq1 5965	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑝 → (𝑢 ↾ suc ℎ) = (𝑝 ↾ suc ℎ))
39	38	eqeq1d 2726	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑝 → ((𝑢 ↾ suc ℎ) = (𝑣 ↾ suc ℎ) ↔ (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))
40	37, 39	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑝 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)) ↔ (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))
41	40	ralbidv 3169	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑝 → (∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)) ↔ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))
42	35, 41	anbi12d 630	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑝 → ((ℎ ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))) ↔ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))))
43	42	cbvrexvw 3227	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ 𝐴 (ℎ ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))) ↔ ∃𝑝 ∈ 𝐴 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))
44	33, 43	bitrdi 287	. . . . . . . . 9 ⊢ (𝑦 = ℎ → (∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑝 ∈ 𝐴 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))))
45	24, 44	elab 3660	. . . . . . . 8 ⊢ (ℎ ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑝 ∈ 𝐴 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))
46	23, 45	bitrdi 287	. . . . . . 7 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → (ℎ ∈ dom 𝑆 ↔ ∃𝑝 ∈ 𝐴 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))))
47	46	3ad2ant1 1130	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → (ℎ ∈ dom 𝑆 ↔ ∃𝑝 ∈ 𝐴 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))))
48		simpl1 1188	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
49		simpl2 1189	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝐴 ⊆ No ∧ 𝐴 ∈ V))
50		simprl 768	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑝 ∈ 𝐴)
51		simprrl 778	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ℎ ∈ dom 𝑝)
52		simprrr 779	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))
53	4	nosupres 27556	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑝 ∈ 𝐴 ∧ ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))) → (𝑆 ↾ suc ℎ) = (𝑝 ↾ suc ℎ))
54	48, 49, 50, 51, 52, 53	syl113anc 1379	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑆 ↾ suc ℎ) = (𝑝 ↾ suc ℎ))
55		simpl2l 1223	. . . . . . . . . . . . . . 15 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝐴 ⊆ No )
56	55, 50	sseldd 3975	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑝 ∈ No )
57	3	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑈 ∈ No )
58		sltso 27525	. . . . . . . . . . . . . . 15 ⊢ <s Or No
59		soasym 5609	. . . . . . . . . . . . . . 15 ⊢ (( <s Or No ∧ (𝑝 ∈ No ∧ 𝑈 ∈ No )) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
60	58, 59	mpan 687	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ∈ No ∧ 𝑈 ∈ No ) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
61	56, 57, 60	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
62		simpl3 1190	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑈 ∈ 𝐴)
63		breq1 5141	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑈 → (𝑣 <s 𝑝 ↔ 𝑈 <s 𝑝))
64	63	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑈 → (¬ 𝑣 <s 𝑝 ↔ ¬ 𝑈 <s 𝑝))
65		reseq1 5965	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑈 → (𝑣 ↾ suc ℎ) = (𝑈 ↾ suc ℎ))
66	65	eqeq2d 2735	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑈 → ((𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ) ↔ (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ)))
67	64, 66	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑈 → ((¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)) ↔ (¬ 𝑈 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ))))
68	67	rspcv 3600	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ 𝐴 → (∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)) → (¬ 𝑈 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ))))
69	62, 52, 68	sylc 65	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (¬ 𝑈 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ)))
70	61, 69	syld 47	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑝 <s 𝑈 → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ)))
71	70	imp 406	. . . . . . . . . . 11 ⊢ ((((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ 𝑝 <s 𝑈) → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ))
72		nodmon 27499	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ No → dom 𝑝 ∈ On)
73	56, 72	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → dom 𝑝 ∈ On)
74		onelon 6379	. . . . . . . . . . . . . . . 16 ⊢ ((dom 𝑝 ∈ On ∧ ℎ ∈ dom 𝑝) → ℎ ∈ On)
75	73, 51, 74	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ℎ ∈ On)
76		onsucb 7798	. . . . . . . . . . . . . . 15 ⊢ (ℎ ∈ On ↔ suc ℎ ∈ On)
77	75, 76	sylib 217	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → suc ℎ ∈ On)
78		noreson 27509	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ No ∧ suc ℎ ∈ On) → (𝑈 ↾ suc ℎ) ∈ No )
79	57, 77, 78	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑈 ↾ suc ℎ) ∈ No )
80		sonr 5601	. . . . . . . . . . . . . 14 ⊢ (( <s Or No ∧ (𝑈 ↾ suc ℎ) ∈ No ) → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
81	58, 80	mpan 687	. . . . . . . . . . . . 13 ⊢ ((𝑈 ↾ suc ℎ) ∈ No → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
82	79, 81	syl 17	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
83	82	adantr 480	. . . . . . . . . . 11 ⊢ ((((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
84	71, 83	eqnbrtrd 5156	. . . . . . . . . 10 ⊢ ((((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ 𝑝 <s 𝑈) → ¬ (𝑝 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
85	84	ex 412	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑝 <s 𝑈 → ¬ (𝑝 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ)))
86		sltres 27511	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ No ∧ 𝑈 ∈ No ∧ suc ℎ ∈ On) → ((𝑝 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ) → 𝑝 <s 𝑈))
87	56, 57, 77, 86	syl3anc 1368	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ((𝑝 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ) → 𝑝 <s 𝑈))
88	87	con3d 152	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (¬ 𝑝 <s 𝑈 → ¬ (𝑝 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ)))
89	85, 88	pm2.61d 179	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ (𝑝 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
90	54, 89	eqnbrtrd 5156	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ (𝑆 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
91	90	rexlimdvaa 3148	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → (∃𝑝 ∈ 𝐴 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))) → ¬ (𝑆 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ)))
92	47, 91	sylbid 239	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → (ℎ ∈ dom 𝑆 → ¬ (𝑆 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ)))
93	92	imp 406	. . . 4 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ ℎ ∈ dom 𝑆) → ¬ (𝑆 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
94		nodmord 27502	. . . . . . . 8 ⊢ (𝑆 ∈ No → Ord dom 𝑆)
95		ordsucss 7799	. . . . . . . 8 ⊢ (Ord dom 𝑆 → (ℎ ∈ dom 𝑆 → suc ℎ ⊆ dom 𝑆))
96	6, 94, 95	3syl 18	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → (ℎ ∈ dom 𝑆 → suc ℎ ⊆ dom 𝑆))
97	96	imp 406	. . . . . 6 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ ℎ ∈ dom 𝑆) → suc ℎ ⊆ dom 𝑆)
98	97	resabs1d 6002	. . . . 5 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ ℎ ∈ dom 𝑆) → ((𝑈 ↾ dom 𝑆) ↾ suc ℎ) = (𝑈 ↾ suc ℎ))
99	98	breq2d 5150	. . . 4 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ ℎ ∈ dom 𝑆) → ((𝑆 ↾ suc ℎ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ℎ) ↔ (𝑆 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ)))
100	93, 99	mtbird 325	. . 3 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) ∧ ℎ ∈ dom 𝑆) → ¬ (𝑆 ↾ suc ℎ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ℎ))
101	100	ralrimiva 3138	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → ∀ℎ ∈ dom 𝑆 ¬ (𝑆 ↾ suc ℎ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ℎ))
102		noresle 27546	. 2 ⊢ ((((𝑈 ↾ dom 𝑆) ∈ No ∧ 𝑆 ∈ No ) ∧ (dom (𝑈 ↾ dom 𝑆) ⊆ dom 𝑆 ∧ dom 𝑆 ⊆ dom 𝑆 ∧ ∀ℎ ∈ dom 𝑆 ¬ (𝑆 ↾ suc ℎ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ℎ))) → ¬ 𝑆 <s (𝑈 ↾ dom 𝑆))
103	10, 6, 14, 15, 101, 102	syl23anc 1374	1 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ 𝑈 ∈ 𝐴) → ¬ 𝑆 <s (𝑈 ↾ dom 𝑆))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 {cab 2701 ∀wral 3053 ∃wrex 3062 Vcvv 3466 ∪ cun 3938 ∩ cin 3939 ⊆ wss 3940 ifcif 4520 {csn 4620 ⟨cop 4626 class class class wbr 5138 ↦ cmpt 5221 Or wor 5577 dom cdm 5666 ↾ cres 5668 Ord word 6353 Oncon0 6354 suc csuc 6356 ℩cio 6483 ‘cfv 6533 ℩crio 7356 2_oc2o 8455 No csur 27489 <s cslt 27490

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pr 5417 ax-un 7718

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-rmo 3368 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-tp 4625 df-op 4627 df-uni 4900 df-int 4941 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-ord 6357 df-on 6358 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7357 df-1o 8461 df-2o 8462 df-no 27492 df-slt 27493 df-bday 27494

This theorem is referenced by: nosupbnd1lem2 27558 nosupbnd1lem6 27562

W3C validator