Theorem noinfbnd1lem1 33523

Description: Lemma for noinfbnd1 33529. Establish a soft lower bound. (Contributed by Scott Fenton, 9-Aug-2024.)

Hypothesis

Ref	Expression
noinfbnd1.1	⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))

Assertion

Ref	Expression
noinfbnd1lem1	⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇)

Distinct variable groups:   𝐵,𝑔,𝑢,𝑣,𝑥,𝑦   𝑣,𝑈   𝑥,𝑢,𝑦   𝑔,𝑉   𝑥,𝑣,𝑦

Allowed substitution hints:   𝑇(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑈(𝑥,𝑦,𝑢,𝑔)   𝑉(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem noinfbnd1lem1

Dummy variables ℎ 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		noinfbnd1.1	. . . 4 ⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
2	1	noinfno 33518	. . 3 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → 𝑇 ∈ No )
3	2	3ad2ant2 1131	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → 𝑇 ∈ No )
4		simp2l 1196	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → 𝐵 ⊆ No )
5		simp3 1135	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → 𝑈 ∈ 𝐵)
6	4, 5	sseldd 3895	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → 𝑈 ∈ No )
7		nodmon 33450	. . . 4 ⊢ (𝑇 ∈ No → dom 𝑇 ∈ On)
8	3, 7	syl 17	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → dom 𝑇 ∈ On)
9		noreson 33460	. . 3 ⊢ ((𝑈 ∈ No ∧ dom 𝑇 ∈ On) → (𝑈 ↾ dom 𝑇) ∈ No )
10	6, 8, 9	syl2anc 587	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (𝑈 ↾ dom 𝑇) ∈ No )
11		ssidd 3917	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → dom 𝑇 ⊆ dom 𝑇)
12		dmres 5850	. . . 4 ⊢ dom (𝑈 ↾ dom 𝑇) = (dom 𝑇 ∩ dom 𝑈)
13		inss1 4135	. . . 4 ⊢ (dom 𝑇 ∩ dom 𝑈) ⊆ dom 𝑇
14	12, 13	eqsstri 3928	. . 3 ⊢ dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇
15	14	a1i 11	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇)
16		nodmord 33453	. . . . . . . 8 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
17	3, 16	syl 17	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → Ord dom 𝑇)
18		ordsucss 7538	. . . . . . 7 ⊢ (Ord dom 𝑇 → (ℎ ∈ dom 𝑇 → suc ℎ ⊆ dom 𝑇))
19	17, 18	syl 17	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (ℎ ∈ dom 𝑇 → suc ℎ ⊆ dom 𝑇))
20	19	imp 410	. . . . 5 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ ℎ ∈ dom 𝑇) → suc ℎ ⊆ dom 𝑇)
21	20	resabs1d 5859	. . . 4 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ ℎ ∈ dom 𝑇) → ((𝑈 ↾ dom 𝑇) ↾ suc ℎ) = (𝑈 ↾ suc ℎ))
22	1	noinfdm 33519	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {ℎ ∣ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)))})
23	22	eleq2d 2837	. . . . . . . 8 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (ℎ ∈ dom 𝑇 ↔ ℎ ∈ {ℎ ∣ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)))}))
24		abid 2739	. . . . . . . . 9 ⊢ (ℎ ∈ {ℎ ∣ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)))} ↔ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ))))
25		breq2 5040	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑣 → (𝑝 <s 𝑞 ↔ 𝑝 <s 𝑣))
26	25	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑣 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣))
27		reseq1 5822	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑣 → (𝑞 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))
28	27	eqeq2d 2769	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑣 → ((𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ) ↔ (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))
29	26, 28	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑣 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))
30	29	cbvralvw 3361	. . . . . . . . . . 11 ⊢ (∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))
31	30	anbi2i 625	. . . . . . . . . 10 ⊢ ((ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ))) ↔ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))
32	31	rexbii 3175	. . . . . . . . 9 ⊢ (∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ))) ↔ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))
33	24, 32	bitri 278	. . . . . . . 8 ⊢ (ℎ ∈ {ℎ ∣ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)))} ↔ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))
34	23, 33	bitrdi 290	. . . . . . 7 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (ℎ ∈ dom 𝑇 ↔ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))))
35	34	3ad2ant1 1130	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (ℎ ∈ dom 𝑇 ↔ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))))
36		simpl2l 1223	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝐵 ⊆ No )
37		simprl 770	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑝 ∈ 𝐵)
38	36, 37	sseldd 3895	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑝 ∈ No )
39	6	adantr 484	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑈 ∈ No )
40		sltso 33476	. . . . . . . . . . . 12 ⊢ <s Or No
41		soasym 5477	. . . . . . . . . . . 12 ⊢ (( <s Or No ∧ (𝑝 ∈ No ∧ 𝑈 ∈ No )) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
42	40, 41	mpan 689	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ No ∧ 𝑈 ∈ No ) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
43	38, 39, 42	syl2anc 587	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
44		nodmon 33450	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ No → dom 𝑝 ∈ On)
45	38, 44	syl 17	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → dom 𝑝 ∈ On)
46		simprrl 780	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ℎ ∈ dom 𝑝)
47		onelon 6199	. . . . . . . . . . . . 13 ⊢ ((dom 𝑝 ∈ On ∧ ℎ ∈ dom 𝑝) → ℎ ∈ On)
48	45, 46, 47	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ℎ ∈ On)
49		sucelon 7537	. . . . . . . . . . . 12 ⊢ (ℎ ∈ On ↔ suc ℎ ∈ On)
50	48, 49	sylib 221	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → suc ℎ ∈ On)
51		sltres 33462	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ No ∧ 𝑝 ∈ No ∧ suc ℎ ∈ On) → ((𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ) → 𝑈 <s 𝑝))
52	39, 38, 50, 51	syl3anc 1368	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ((𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ) → 𝑈 <s 𝑝))
53	43, 52	nsyld 159	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑝 <s 𝑈 → ¬ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ)))
54		noreson 33460	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ No ∧ suc ℎ ∈ On) → (𝑈 ↾ suc ℎ) ∈ No )
55	39, 50, 54	syl2anc 587	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑈 ↾ suc ℎ) ∈ No )
56		sonr 5469	. . . . . . . . . . . . . 14 ⊢ (( <s Or No ∧ (𝑈 ↾ suc ℎ) ∈ No ) → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
57	40, 56	mpan 689	. . . . . . . . . . . . 13 ⊢ ((𝑈 ↾ suc ℎ) ∈ No → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
58	55, 57	syl 17	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
59	58	adantr 484	. . . . . . . . . . 11 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ ¬ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
60		breq2 5040	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑈 → (𝑝 <s 𝑣 ↔ 𝑝 <s 𝑈))
61	60	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑈 → (¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑈))
62		reseq1 5822	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑈 → (𝑣 ↾ suc ℎ) = (𝑈 ↾ suc ℎ))
63	62	eqeq2d 2769	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑈 → ((𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ) ↔ (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ)))
64	61, 63	imbi12d 348	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑈 → ((¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)) ↔ (¬ 𝑝 <s 𝑈 → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ))))
65		simprrr 781	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))
66		simpl3 1190	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑈 ∈ 𝐵)
67	64, 65, 66	rspcdva 3545	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (¬ 𝑝 <s 𝑈 → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ)))
68	67	imp 410	. . . . . . . . . . . 12 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ ¬ 𝑝 <s 𝑈) → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ))
69	68	breq2d 5048	. . . . . . . . . . 11 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ ¬ 𝑝 <s 𝑈) → ((𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ) ↔ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ)))
70	59, 69	mtbird 328	. . . . . . . . . 10 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ ¬ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ))
71	70	ex 416	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (¬ 𝑝 <s 𝑈 → ¬ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ)))
72	53, 71	pm2.61d 182	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ))
73		simpl1 1188	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
74		simpl2 1189	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
75	1	noinfres 33522	. . . . . . . . . 10 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑝 ∈ 𝐵 ∧ ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))) → (𝑇 ↾ suc ℎ) = (𝑝 ↾ suc ℎ))
76	73, 74, 37, 46, 65, 75	syl113anc 1379	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑇 ↾ suc ℎ) = (𝑝 ↾ suc ℎ))
77	76	breq2d 5048	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ((𝑈 ↾ suc ℎ) <s (𝑇 ↾ suc ℎ) ↔ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ)))
78	72, 77	mtbird 328	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ (𝑈 ↾ suc ℎ) <s (𝑇 ↾ suc ℎ))
79	78	rexlimdvaa 3209	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))) → ¬ (𝑈 ↾ suc ℎ) <s (𝑇 ↾ suc ℎ)))
80	35, 79	sylbid 243	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (ℎ ∈ dom 𝑇 → ¬ (𝑈 ↾ suc ℎ) <s (𝑇 ↾ suc ℎ)))
81	80	imp 410	. . . 4 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ ℎ ∈ dom 𝑇) → ¬ (𝑈 ↾ suc ℎ) <s (𝑇 ↾ suc ℎ))
82	21, 81	eqnbrtrd 5054	. . 3 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ ℎ ∈ dom 𝑇) → ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ℎ) <s (𝑇 ↾ suc ℎ))
83	82	ralrimiva 3113	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → ∀ℎ ∈ dom 𝑇 ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ℎ) <s (𝑇 ↾ suc ℎ))
84		noresle 33497	. 2 ⊢ (((𝑇 ∈ No ∧ (𝑈 ↾ dom 𝑇) ∈ No ) ∧ (dom 𝑇 ⊆ dom 𝑇 ∧ dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇 ∧ ∀ℎ ∈ dom 𝑇 ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ℎ) <s (𝑇 ↾ suc ℎ))) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇)
85	3, 10, 11, 15, 83, 84	syl23anc 1374	1 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {cab 2735  ∀wral 3070  ∃wrex 3071   ∪ cun 3858   ∩ cin 3859   ⊆ wss 3860  ifcif 4423  {csn 4525  ⟨cop 4531   class class class wbr 5036   ↦ cmpt 5116   Or wor 5446  dom cdm 5528   ↾ cres 5530  Ord word 6173  Oncon0 6174  suc csuc 6176  ℩cio 6297  ‘cfv 6340  ℩crio 7113  1_oc1o 8111   No csur 33440   <s cslt 33441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5160  ax-sep 5173  ax-nul 5180  ax-pr 5302  ax-un 7465

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-tr 5143  df-id 5434  df-eprel 5439  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-ord 6177  df-on 6178  df-suc 6180  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-1o 8118  df-2o 8119  df-no 33443  df-slt 33444  df-bday 33445

This theorem is referenced by:  noinfbnd1lem2  33524  noinfbnd1lem6  33528