noinfbnd1lem4 - Metamath Proof Explorer

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

Theorem noinfbnd1lem4 27614

Description: Lemma for noinfbnd1 27617. If 𝑈 is a prolongment of 𝑇 and in 𝐵, then (𝑈‘dom 𝑇) is not undefined. (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
noinfbnd1lem4	⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ ∅)

Distinct variable groups: 𝐵,𝑔,𝑢,𝑣,𝑥,𝑦 𝑣,𝑈 𝑥,𝑢,𝑦 𝑔,𝑉 𝑥,𝑣,𝑦,𝑈 Allowed substitution hints: 𝑇(𝑥,𝑦,𝑣,𝑢,𝑔) 𝑈(𝑢,𝑔) 𝑉(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem noinfbnd1lem4 Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl1 1188	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
2		simpl2 1189	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
3		simprl 768	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑤 ∈ 𝐵)
4		simpl3 1190	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
5		simp2l 1196	. . . . . . . . . . . . 13 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝐵 ⊆ No )
6	5	sselda 3977	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ No )
7		simp3l 1198	. . . . . . . . . . . . . 14 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑈 ∈ 𝐵)
8	5, 7	sseldd 3978	. . . . . . . . . . . . 13 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑈 ∈ No )
9	8	adantr 480	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → 𝑈 ∈ No )
10		sltso 27564	. . . . . . . . . . . . 13 ⊢ <s Or No
11		soasym 5612	. . . . . . . . . . . . 13 ⊢ (( <s Or No ∧ (𝑤 ∈ No ∧ 𝑈 ∈ No )) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤))
12	10, 11	mpan 687	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ No ∧ 𝑈 ∈ No ) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤))
13	6, 9, 12	syl2anc 583	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤))
14	13	impr 454	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ 𝑈 <s 𝑤)
15	3, 14	jca 511	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑤))
16		noinfbnd1.1	. . . . . . . . . 10 ⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
17	16	noinfbnd1lem2 27612	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ ((𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇) ∧ (𝑤 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑤))) → (𝑤 ↾ dom 𝑇) = 𝑇)
18	1, 2, 4, 15, 17	syl112anc 1371	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ↾ dom 𝑇) = 𝑇)
19	16	noinfbnd1lem3 27613	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑤 ∈ 𝐵 ∧ (𝑤 ↾ dom 𝑇) = 𝑇)) → (𝑤‘dom 𝑇) ≠ 1_o)
20	1, 2, 3, 18, 19	syl112anc 1371	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤‘dom 𝑇) ≠ 1_o)
21	20	neneqd 2939	. . . . . 6 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ (𝑤‘dom 𝑇) = 1_o)
22	21	expr 456	. . . . 5 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → (𝑤 <s 𝑈 → ¬ (𝑤‘dom 𝑇) = 1_o))
23		imnan 399	. . . . 5 ⊢ ((𝑤 <s 𝑈 → ¬ (𝑤‘dom 𝑇) = 1_o) ↔ ¬ (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1_o))
24	22, 23	sylib 217	. . . 4 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → ¬ (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1_o))
25	24	nrexdv 3143	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → ¬ ∃𝑤 ∈ 𝐵 (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1_o))
26		breq2 5145	. . . . . . 7 ⊢ (𝑥 = 𝑈 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝑈))
27	26	rexbidv 3172	. . . . . 6 ⊢ (𝑥 = 𝑈 → (∃𝑦 ∈ 𝐵 𝑦 <s 𝑥 ↔ ∃𝑦 ∈ 𝐵 𝑦 <s 𝑈))
28		simpl1 1188	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
29		dfral2 3093	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥 ↔ ¬ ∃𝑥 ∈ 𝐵 ¬ ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥)
30		ralnex 3066	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ↔ ¬ ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥)
31	30	rexbii 3088	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ↔ ∃𝑥 ∈ 𝐵 ¬ ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥)
32	29, 31	xchbinxr 335	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥 ↔ ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
33	28, 32	sylibr 233	. . . . . 6 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥)
34		simpl3l 1225	. . . . . 6 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → 𝑈 ∈ 𝐵)
35	27, 33, 34	rspcdva 3607	. . . . 5 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∃𝑦 ∈ 𝐵 𝑦 <s 𝑈)
36		breq1 5144	. . . . . 6 ⊢ (𝑦 = 𝑤 → (𝑦 <s 𝑈 ↔ 𝑤 <s 𝑈))
37	36	cbvrexvw 3229	. . . . 5 ⊢ (∃𝑦 ∈ 𝐵 𝑦 <s 𝑈 ↔ ∃𝑤 ∈ 𝐵 𝑤 <s 𝑈)
38	35, 37	sylib 217	. . . 4 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∃𝑤 ∈ 𝐵 𝑤 <s 𝑈)
39		simpl2l 1223	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → 𝐵 ⊆ No )
40	39	adantr 480	. . . . . . . . 9 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝐵 ⊆ No )
41		simprl 768	. . . . . . . . 9 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑤 ∈ 𝐵)
42	40, 41	sseldd 3978	. . . . . . . 8 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑤 ∈ No )
43	34	adantr 480	. . . . . . . . 9 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑈 ∈ 𝐵)
44	40, 43	sseldd 3978	. . . . . . . 8 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑈 ∈ No )
45		simpl2 1189	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
46	16	noinfno 27606	. . . . . . . . . . 11 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → 𝑇 ∈ No )
47	45, 46	syl 17	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → 𝑇 ∈ No )
48	47	adantr 480	. . . . . . . . 9 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑇 ∈ No )
49		nodmon 27538	. . . . . . . . 9 ⊢ (𝑇 ∈ No → dom 𝑇 ∈ On)
50	48, 49	syl 17	. . . . . . . 8 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → dom 𝑇 ∈ On)
51		simpll1 1209	. . . . . . . . . 10 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
52		simpll2 1210	. . . . . . . . . 10 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
53		simpll3 1211	. . . . . . . . . 10 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
54		simprr 770	. . . . . . . . . . . 12 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑤 <s 𝑈)
55	42, 44, 12	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤))
56	54, 55	mpd 15	. . . . . . . . . . 11 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ 𝑈 <s 𝑤)
57	41, 56	jca 511	. . . . . . . . . 10 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑤))
58	51, 52, 53, 57, 17	syl112anc 1371	. . . . . . . . 9 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ↾ dom 𝑇) = 𝑇)
59		simpl3r 1226	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → (𝑈 ↾ dom 𝑇) = 𝑇)
60	59	adantr 480	. . . . . . . . 9 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑈 ↾ dom 𝑇) = 𝑇)
61	58, 60	eqtr4d 2769	. . . . . . . 8 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ↾ dom 𝑇) = (𝑈 ↾ dom 𝑇))
62		simplr 766	. . . . . . . 8 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑈‘dom 𝑇) = ∅)
63		nogt01o 27584	. . . . . . . 8 ⊢ (((𝑤 ∈ No ∧ 𝑈 ∈ No ∧ dom 𝑇 ∈ On) ∧ ((𝑤 ↾ dom 𝑇) = (𝑈 ↾ dom 𝑇) ∧ 𝑤 <s 𝑈) ∧ (𝑈‘dom 𝑇) = ∅) → (𝑤‘dom 𝑇) = 1_o)
64	42, 44, 50, 61, 54, 62, 63	syl321anc 1389	. . . . . . 7 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤‘dom 𝑇) = 1_o)
65	64	expr 456	. . . . . 6 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ 𝑤 ∈ 𝐵) → (𝑤 <s 𝑈 → (𝑤‘dom 𝑇) = 1_o))
66	65	ancld 550	. . . . 5 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ 𝑤 ∈ 𝐵) → (𝑤 <s 𝑈 → (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1_o)))
67	66	reximdva 3162	. . . 4 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → (∃𝑤 ∈ 𝐵 𝑤 <s 𝑈 → ∃𝑤 ∈ 𝐵 (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1_o)))
68	38, 67	mpd 15	. . 3 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∃𝑤 ∈ 𝐵 (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1_o))
69	25, 68	mtand 813	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → ¬ (𝑈‘dom 𝑇) = ∅)
70	69	neqned 2941	1 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ ∅)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 {cab 2703 ≠ wne 2934 ∀wral 3055 ∃wrex 3064 ∪ cun 3941 ⊆ wss 3943 ∅c0 4317 ifcif 4523 {csn 4623 ⟨cop 4629 class class class wbr 5141 ↦ cmpt 5224 Or wor 5580 dom cdm 5669 ↾ cres 5671 Oncon0 6358 suc csuc 6360 ℩cio 6487 ‘cfv 6537 ℩crio 7360 1_oc1o 8460 No csur 27528 <s cslt 27529

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 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pr 5420 ax-un 7722

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 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-uni 4903 df-int 4944 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-ord 6361 df-on 6362 df-suc 6364 df-iota 6489 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7361 df-1o 8467 df-2o 8468 df-no 27531 df-slt 27532 df-bday 27533

This theorem is referenced by: noinfbnd1lem5 27615 noinfbnd1lem6 27616

W3C validator