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 27219

Description: Lemma for noinfbnd1 27222. 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 1192	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
2		simpl2 1193	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
3		simprl 770	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑤 ∈ 𝐵)
4		simpl3 1194	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
5		simp2l 1200	. . . . . . . . . . . . 13 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝐵 ⊆ No )
6	5	sselda 3982	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ No )
7		simp3l 1202	. . . . . . . . . . . . . 14 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑈 ∈ 𝐵)
8	5, 7	sseldd 3983	. . . . . . . . . . . . 13 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑈 ∈ No )
9	8	adantr 482	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → 𝑈 ∈ No )
10		sltso 27169	. . . . . . . . . . . . 13 ⊢ <s Or No
11		soasym 5619	. . . . . . . . . . . . 13 ⊢ (( <s Or No ∧ (𝑤 ∈ No ∧ 𝑈 ∈ No )) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤))
12	10, 11	mpan 689	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ No ∧ 𝑈 ∈ No ) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤))
13	6, 9, 12	syl2anc 585	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤))
14	13	impr 456	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ 𝑈 <s 𝑤)
15	3, 14	jca 513	. . . . . . . . 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 27217	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ ((𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇) ∧ (𝑤 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑤))) → (𝑤 ↾ dom 𝑇) = 𝑇)
18	1, 2, 4, 15, 17	syl112anc 1375	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ↾ dom 𝑇) = 𝑇)
19	16	noinfbnd1lem3 27218	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑤 ∈ 𝐵 ∧ (𝑤 ↾ dom 𝑇) = 𝑇)) → (𝑤‘dom 𝑇) ≠ 1_o)
20	1, 2, 3, 18, 19	syl112anc 1375	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤‘dom 𝑇) ≠ 1_o)
21	20	neneqd 2946	. . . . . 6 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ (𝑤‘dom 𝑇) = 1_o)
22	21	expr 458	. . . . 5 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → (𝑤 <s 𝑈 → ¬ (𝑤‘dom 𝑇) = 1_o))
23		imnan 401	. . . . 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 3150	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → ¬ ∃𝑤 ∈ 𝐵 (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1_o))
26		breq2 5152	. . . . . . 7 ⊢ (𝑥 = 𝑈 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝑈))
27	26	rexbidv 3179	. . . . . 6 ⊢ (𝑥 = 𝑈 → (∃𝑦 ∈ 𝐵 𝑦 <s 𝑥 ↔ ∃𝑦 ∈ 𝐵 𝑦 <s 𝑈))
28		simpl1 1192	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
29		dfral2 3100	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥 ↔ ¬ ∃𝑥 ∈ 𝐵 ¬ ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥)
30		ralnex 3073	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ↔ ¬ ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥)
31	30	rexbii 3095	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ↔ ∃𝑥 ∈ 𝐵 ¬ ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥)
32	29, 31	xchbinxr 335	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥 ↔ ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
33	28, 32	sylibr 233	. . . . . 6 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥)
34		simpl3l 1229	. . . . . 6 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → 𝑈 ∈ 𝐵)
35	27, 33, 34	rspcdva 3614	. . . . 5 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∃𝑦 ∈ 𝐵 𝑦 <s 𝑈)
36		breq1 5151	. . . . . 6 ⊢ (𝑦 = 𝑤 → (𝑦 <s 𝑈 ↔ 𝑤 <s 𝑈))
37	36	cbvrexvw 3236	. . . . 5 ⊢ (∃𝑦 ∈ 𝐵 𝑦 <s 𝑈 ↔ ∃𝑤 ∈ 𝐵 𝑤 <s 𝑈)
38	35, 37	sylib 217	. . . 4 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∃𝑤 ∈ 𝐵 𝑤 <s 𝑈)
39		simpl2l 1227	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → 𝐵 ⊆ No )
40	39	adantr 482	. . . . . . . . 9 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝐵 ⊆ No )
41		simprl 770	. . . . . . . . 9 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑤 ∈ 𝐵)
42	40, 41	sseldd 3983	. . . . . . . 8 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑤 ∈ No )
43	34	adantr 482	. . . . . . . . 9 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑈 ∈ 𝐵)
44	40, 43	sseldd 3983	. . . . . . . 8 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑈 ∈ No )
45		simpl2 1193	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
46	16	noinfno 27211	. . . . . . . . . . 11 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → 𝑇 ∈ No )
47	45, 46	syl 17	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → 𝑇 ∈ No )
48	47	adantr 482	. . . . . . . . 9 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑇 ∈ No )
49		nodmon 27143	. . . . . . . . 9 ⊢ (𝑇 ∈ No → dom 𝑇 ∈ On)
50	48, 49	syl 17	. . . . . . . 8 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → dom 𝑇 ∈ On)
51		simpll1 1213	. . . . . . . . . 10 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
52		simpll2 1214	. . . . . . . . . 10 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
53		simpll3 1215	. . . . . . . . . 10 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
54		simprr 772	. . . . . . . . . . . 12 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑤 <s 𝑈)
55	42, 44, 12	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤))
56	54, 55	mpd 15	. . . . . . . . . . 11 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ 𝑈 <s 𝑤)
57	41, 56	jca 513	. . . . . . . . . 10 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑤))
58	51, 52, 53, 57, 17	syl112anc 1375	. . . . . . . . 9 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ↾ dom 𝑇) = 𝑇)
59		simpl3r 1230	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → (𝑈 ↾ dom 𝑇) = 𝑇)
60	59	adantr 482	. . . . . . . . 9 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑈 ↾ dom 𝑇) = 𝑇)
61	58, 60	eqtr4d 2776	. . . . . . . 8 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ↾ dom 𝑇) = (𝑈 ↾ dom 𝑇))
62		simplr 768	. . . . . . . 8 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑈‘dom 𝑇) = ∅)
63		nogt01o 27189	. . . . . . . 8 ⊢ (((𝑤 ∈ No ∧ 𝑈 ∈ No ∧ dom 𝑇 ∈ On) ∧ ((𝑤 ↾ dom 𝑇) = (𝑈 ↾ dom 𝑇) ∧ 𝑤 <s 𝑈) ∧ (𝑈‘dom 𝑇) = ∅) → (𝑤‘dom 𝑇) = 1_o)
64	42, 44, 50, 61, 54, 62, 63	syl321anc 1393	. . . . . . 7 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤‘dom 𝑇) = 1_o)
65	64	expr 458	. . . . . 6 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ 𝑤 ∈ 𝐵) → (𝑤 <s 𝑈 → (𝑤‘dom 𝑇) = 1_o))
66	65	ancld 552	. . . . 5 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ 𝑤 ∈ 𝐵) → (𝑤 <s 𝑈 → (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1_o)))
67	66	reximdva 3169	. . . 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 815	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → ¬ (𝑈‘dom 𝑇) = ∅)
70	69	neqned 2948	1 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ ∅)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 {cab 2710 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 ∪ cun 3946 ⊆ wss 3948 ∅c0 4322 ifcif 4528 {csn 4628 ⟨cop 4634 class class class wbr 5148 ↦ cmpt 5231 Or wor 5587 dom cdm 5676 ↾ cres 5678 Oncon0 6362 suc csuc 6364 ℩cio 6491 ‘cfv 6541 ℩crio 7361 1_oc1o 8456 No csur 27133 <s cslt 27134

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pr 5427 ax-un 7722

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-ord 6365 df-on 6366 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7362 df-1o 8463 df-2o 8464 df-no 27136 df-slt 27137 df-bday 27138

This theorem is referenced by: noinfbnd1lem5 27220 noinfbnd1lem6 27221

W3C validator