noinfbnd1lem1 - Metamath Proof Explorer

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

Theorem noinfbnd1lem1 27853

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

**Hypothesis**
Ref	Expression
noinfbnd1.1	⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ 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 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
2	1	noinfno 27848	. . 3 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → 𝑇 ∈ No )
3	2	3ad2ant2 1150	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → 𝑇 ∈ No )
4		simp2l 1216	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → 𝐵 ⊆ No )
5		simp3 1154	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → 𝑈 ∈ 𝐵)
6	4, 5	sseldd 3944	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → 𝑈 ∈ No )
7		nodmon 27780	. . . 4 ⊢ (𝑇 ∈ No → dom 𝑇 ∈ On)
8	3, 7	syl 18	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → dom 𝑇 ∈ On)
9		noreson 27790	. . 3 ⊢ ((𝑈 ∈ No ∧ dom 𝑇 ∈ On) → (𝑈 ↾ dom 𝑇) ∈ No )
10	6, 8, 9	syl2anc 595	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (𝑈 ↾ dom 𝑇) ∈ No )
11		ssidd 3966	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → dom 𝑇 ⊆ dom 𝑇)
12		dmres 6012	. . . 4 ⊢ dom (𝑈 ↾ dom 𝑇) = (dom 𝑇 ∩ dom 𝑈)
13		inss1 4195	. . . 4 ⊢ (dom 𝑇 ∩ dom 𝑈) ⊆ dom 𝑇
14	12, 13	eqsstri 3989	. . 3 ⊢ dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇
15	14	a1i 11	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇)
16		nodmord 27783	. . . . . . . 8 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
17	3, 16	syl 18	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → Ord dom 𝑇)
18		ordsucss 7814	. . . . . . 7 ⊢ (Ord dom 𝑇 → (ℎ ∈ dom 𝑇 → suc ℎ ⊆ dom 𝑇))
19	17, 18	syl 18	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (ℎ ∈ dom 𝑇 → suc ℎ ⊆ dom 𝑇))
20	19	imp 411	. . . . 5 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ ℎ ∈ dom 𝑇) → suc ℎ ⊆ dom 𝑇)
21	20	resabs1d 6008	. . . 4 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ ℎ ∈ dom 𝑇) → ((𝑈 ↾ dom 𝑇) ↾ suc ℎ) = (𝑈 ↾ suc ℎ))
22	1	noinfdm 27849	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {ℎ ∣ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)))})
23	22	eleq2d 2855	. . . . . . . 8 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (ℎ ∈ dom 𝑇 ↔ ℎ ∈ {ℎ ∣ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)))}))
24		abid 2751	. . . . . . . . 9 ⊢ (ℎ ∈ {ℎ ∣ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)))} ↔ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ))))
25		breq2 5115	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑣 → (𝑝 <s 𝑞 ↔ 𝑝 <s 𝑣))
26	25	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑣 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣))
27		reseq1 5973	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑣 → (𝑞 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))
28	27	eqeq2d 2780	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑣 → ((𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ) ↔ (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))
29	26, 28	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑣 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))
30	29	cbvralvw 3249	. . . . . . . . . . 11 ⊢ (∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))
31	30	anbi2i 634	. . . . . . . . . 10 ⊢ ((ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ))) ↔ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))
32	31	rexbii 3118	. . . . . . . . 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 1149	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (ℎ ∈ dom 𝑇 ↔ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))))
36		simpl2l 1243	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝐵 ⊆ No )
37		simprl 782	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑝 ∈ 𝐵)
38	36, 37	sseldd 3944	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑝 ∈ No )
39	6	adantr 485	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑈 ∈ No )
40		ltsso 27806	. . . . . . . . . . . 12 ⊢ <s Or No
41		soasym 5603	. . . . . . . . . . . 12 ⊢ (( <s Or No ∧ (𝑝 ∈ No ∧ 𝑈 ∈ No )) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
42	40, 41	mpan 702	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ No ∧ 𝑈 ∈ No ) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
43	38, 39, 42	syl2anc 595	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
44		nodmon 27780	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ No → dom 𝑝 ∈ On)
45	38, 44	syl 18	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → dom 𝑝 ∈ On)
46		simprrl 792	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ℎ ∈ dom 𝑝)
47		onelon 6386	. . . . . . . . . . . . 13 ⊢ ((dom 𝑝 ∈ On ∧ ℎ ∈ dom 𝑝) → ℎ ∈ On)
48	45, 46, 47	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ℎ ∈ On)
49		onsucb 7813	. . . . . . . . . . . 12 ⊢ (ℎ ∈ On ↔ suc ℎ ∈ On)
50	48, 49	sylib 221	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → suc ℎ ∈ On)
51		ltsres 27792	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ No ∧ 𝑝 ∈ No ∧ suc ℎ ∈ On) → ((𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ) → 𝑈 <s 𝑝))
52	39, 38, 50, 51	syl3anc 1396	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ((𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ) → 𝑈 <s 𝑝))
53	43, 52	nsyld 157	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑝 <s 𝑈 → ¬ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ)))
54		noreson 27790	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ No ∧ suc ℎ ∈ On) → (𝑈 ↾ suc ℎ) ∈ No )
55	39, 50, 54	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑈 ↾ suc ℎ) ∈ No )
56		sonr 5594	. . . . . . . . . . . . . 14 ⊢ (( <s Or No ∧ (𝑈 ↾ suc ℎ) ∈ No ) → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
57	40, 56	mpan 702	. . . . . . . . . . . . 13 ⊢ ((𝑈 ↾ suc ℎ) ∈ No → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
58	55, 57	syl 18	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
59	58	adantr 485	. . . . . . . . . . 11 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ ¬ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))
60		breq2 5115	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑈 → (𝑝 <s 𝑣 ↔ 𝑝 <s 𝑈))
61	60	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑈 → (¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑈))
62		reseq1 5973	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑈 → (𝑣 ↾ suc ℎ) = (𝑈 ↾ suc ℎ))
63	62	eqeq2d 2780	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = 𝑈 → ((𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ) ↔ (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ)))
64	61, 63	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑈 → ((¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)) ↔ (¬ 𝑝 <s 𝑈 → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ))))
65		simprrr 793	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))
66		simpl3 1210	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑈 ∈ 𝐵)
67	64, 65, 66	rspcdva 3589	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (¬ 𝑝 <s 𝑈 → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ)))
68	67	imp 411	. . . . . . . . . . . 12 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ ¬ 𝑝 <s 𝑈) → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ))
69	68	breq2d 5123	. . . . . . . . . . 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 417	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (¬ 𝑝 <s 𝑈 → ¬ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ)))
72	53, 71	pm2.61d 181	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ))
73		simpl1 1208	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
74		simpl2 1209	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
75	1	noinfres 27852	. . . . . . . . . 10 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑝 ∈ 𝐵 ∧ ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))) → (𝑇 ↾ suc ℎ) = (𝑝 ↾ suc ℎ))
76	73, 74, 37, 46, 65, 75	syl113anc 1407	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑇 ↾ suc ℎ) = (𝑝 ↾ suc ℎ))
77	76	breq2d 5123	. . . . . . . 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 3173	. . . . . 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 411	. . . 4 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ ℎ ∈ dom 𝑇) → ¬ (𝑈 ↾ suc ℎ) <s (𝑇 ↾ suc ℎ))
82	21, 81	eqnbrtrd 5131	. . 3 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ ℎ ∈ dom 𝑇) → ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ℎ) <s (𝑇 ↾ suc ℎ))
83	82	ralrimiva 3163	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → ∀ℎ ∈ dom 𝑇 ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ℎ) <s (𝑇 ↾ suc ℎ))
84		noresle 27827	. 2 ⊢ (((𝑇 ∈ No ∧ (𝑈 ↾ dom 𝑇) ∈ No ) ∧ (dom 𝑇 ⊆ dom 𝑇 ∧ dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇 ∧ ∀ℎ ∈ dom 𝑇 ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ℎ) <s (𝑇 ↾ suc ℎ))) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇)
85	3, 10, 11, 15, 83, 84	syl23anc 1402	1 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 {cab 2747 ∀wral 3085 ∃wrex 3095 ∪ cun 3909 ∩ cin 3910 ⊆ wss 3911 ifcif 4490 {csn 4592 ⟨cop 4598 class class class wbr 5111 ↦ cmpt 5194 Or wor 5569 dom cdm 5662 ↾ cres 5664 Ord word 6360 Oncon0 6361 suc csuc 6363 ℩cio 6491 ‘cfv 6537 ℩crio 7367 1_oc1o 8446 No csur 27770 <s clts 27771

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rmo 3375 df-reu 3376 df-rab 3423 df-v 3463 df-sbc 3752 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4915 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-ord 6364 df-on 6365 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-fo 6543 df-fv 6545 df-riota 7368 df-1o 8453 df-2o 8454 df-no 27773 df-lts 27774 df-bday 27775

This theorem is referenced by: noinfbnd1lem2 27854 noinfbnd1lem6 27858

W3C validator