noinfbnd1lem5 - Metamath Proof Explorer

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

Theorem noinfbnd1lem5 27995

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

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

Proof of Theorem noinfbnd1lem5 Dummy variables 𝑝 𝑧 𝑎 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		noinfbnd1.1	. . . . . . . . 9 ⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
2	1	noinfno 27986	. . . . . . . 8 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → 𝑇 ∈ No )
3	2	3ad2ant2 1152	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑇 ∈ No )
4	3	adantl 487	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑇 ∈ No )
5		nodmord 27921	. . . . . 6 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
6	4, 5	syl 18	. . . . 5 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → Ord dom 𝑇)
7		ordirr 6377	. . . . 5 ⊢ (Ord dom 𝑇 → ¬ dom 𝑇 ∈ dom 𝑇)
8	6, 7	syl 18	. . . 4 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ dom 𝑇 ∈ dom 𝑇)
9		simpr3l 1253	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑈 ∈ 𝐵)
10	9	adantr 486	. . . . . . 7 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → 𝑈 ∈ 𝐵)
11		ndmfv 6913	. . . . . . . . . . 11 ⊢ (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) = ∅)
12		2on0 8477	. . . . . . . . . . . . 13 ⊢ 2_o ≠ ∅
13	12	necomi 3009	. . . . . . . . . . . 12 ⊢ ∅ ≠ 2_o
14		neeq1 3017	. . . . . . . . . . . 12 ⊢ ((𝑈‘dom 𝑇) = ∅ → ((𝑈‘dom 𝑇) ≠ 2_o ↔ ∅ ≠ 2_o))
15	13, 14	mpbiri 261	. . . . . . . . . . 11 ⊢ ((𝑈‘dom 𝑇) = ∅ → (𝑈‘dom 𝑇) ≠ 2_o)
16	11, 15	syl 18	. . . . . . . . . 10 ⊢ (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) ≠ 2_o)
17	16	neneqd 2960	. . . . . . . . 9 ⊢ (¬ dom 𝑇 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑇) = 2_o)
18	17	con4i 115	. . . . . . . 8 ⊢ ((𝑈‘dom 𝑇) = 2_o → dom 𝑇 ∈ dom 𝑈)
19	18	adantl 487	. . . . . . 7 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 ∈ dom 𝑈)
20		simpl2l 1245	. . . . . . . . . . . . . . . . 17 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) → 𝐵 ⊆ No )
21	20	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝐵 ⊆ No )
22		simpl3l 1247	. . . . . . . . . . . . . . . . 17 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) → 𝑈 ∈ 𝐵)
23	22	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑈 ∈ 𝐵)
24	21, 23	sseldd 3932	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑈 ∈ No )
25		nofun 27917	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ No → Fun 𝑈)
26	24, 25	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → Fun 𝑈)
27		simprll 791	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑧 ∈ 𝐵)
28	21, 27	sseldd 3932	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑧 ∈ No )
29		nofun 27917	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ No → Fun 𝑧)
30	28, 29	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → Fun 𝑧)
31		simpl3r 1248	. . . . . . . . . . . . . . . 16 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) → (𝑈 ↾ dom 𝑇) = 𝑇)
32	31	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈 ↾ dom 𝑇) = 𝑇)
33		simpll1 1231	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
34		simpll2 1232	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
35		simpll3 1233	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
36		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧))
37	1	noinfbnd1lem2 27992	. . . . . . . . . . . . . . . 16 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ ((𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧))) → (𝑧 ↾ dom 𝑇) = 𝑇)
38	33, 34, 35, 36, 37	syl112anc 1401	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑧 ↾ dom 𝑇) = 𝑇)
39	32, 38	eqtr4d 2798	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈 ↾ dom 𝑇) = (𝑧 ↾ dom 𝑇))
40		simplr 781	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈‘dom 𝑇) = 2_o)
41	40, 18	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → dom 𝑇 ∈ dom 𝑈)
42		simprr 785	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑧‘dom 𝑇) = 2_o)
43		ndmfv 6913	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) = ∅)
44		neeq1 3017	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧‘dom 𝑇) = ∅ → ((𝑧‘dom 𝑇) ≠ 2_o ↔ ∅ ≠ 2_o))
45	13, 44	mpbiri 261	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧‘dom 𝑇) = ∅ → (𝑧‘dom 𝑇) ≠ 2_o)
46	43, 45	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) ≠ 2_o)
47	46	neneqd 2960	. . . . . . . . . . . . . . . 16 ⊢ (¬ dom 𝑇 ∈ dom 𝑧 → ¬ (𝑧‘dom 𝑇) = 2_o)
48	47	con4i 115	. . . . . . . . . . . . . . 15 ⊢ ((𝑧‘dom 𝑇) = 2_o → dom 𝑇 ∈ dom 𝑧)
49	42, 48	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → dom 𝑇 ∈ dom 𝑧)
50	40, 42	eqtr4d 2798	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))
51		eqfunressuc 7367	. . . . . . . . . . . . . 14 ⊢ (((Fun 𝑈 ∧ Fun 𝑧) ∧ (𝑈 ↾ dom 𝑇) = (𝑧 ↾ dom 𝑇) ∧ (dom 𝑇 ∈ dom 𝑈 ∧ dom 𝑇 ∈ dom 𝑧 ∧ (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))) → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))
52	26, 30, 39, 41, 49, 50, 51	syl213anc 1416	. . . . . . . . . . . . 13 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))
53	52	expr 462	. . . . . . . . . . . 12 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧)) → ((𝑧‘dom 𝑇) = 2_o → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
54	53	expr 462	. . . . . . . . . . 11 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ 𝑧 ∈ 𝐵) → (¬ 𝑈 <s 𝑧 → ((𝑧‘dom 𝑇) = 2_o → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
55	54	a2d 30	. . . . . . . . . 10 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ 𝑧 ∈ 𝐵) → ((¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) → (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
56	55	ralimdva 3174	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) → (∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) → ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
57	56	impcom 413	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o)) → ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
58	57	anassrs 473	. . . . . . 7 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
59		dmeq 5889	. . . . . . . . . 10 ⊢ (𝑝 = 𝑈 → dom 𝑝 = dom 𝑈)
60	59	eleq2d 2846	. . . . . . . . 9 ⊢ (𝑝 = 𝑈 → (dom 𝑇 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑈))
61		breq1 5106	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑈 → (𝑝 <s 𝑧 ↔ 𝑈 <s 𝑧))
62	61	notbid 321	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑈 → (¬ 𝑝 <s 𝑧 ↔ ¬ 𝑈 <s 𝑧))
63		reseq1 5968	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑈 → (𝑝 ↾ suc dom 𝑇) = (𝑈 ↾ suc dom 𝑇))
64	63	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑈 → ((𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇) ↔ (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
65	62, 64	imbi12d 347	. . . . . . . . . 10 ⊢ (𝑝 = 𝑈 → ((¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)) ↔ (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
66	65	ralbidv 3185	. . . . . . . . 9 ⊢ (𝑝 = 𝑈 → (∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)) ↔ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
67	60, 66	anbi12d 644	. . . . . . . 8 ⊢ (𝑝 = 𝑈 → ((dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))) ↔ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
68	67	rspcev 3576	. . . . . . 7 ⊢ ((𝑈 ∈ 𝐵 ∧ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))) → ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
69	10, 19, 58, 68	syl12anc 850	. . . . . 6 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
70		nodmon 27918	. . . . . . . . 9 ⊢ (𝑇 ∈ No → dom 𝑇 ∈ On)
71	4, 70	syl 18	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → dom 𝑇 ∈ On)
72	71	adantr 486	. . . . . . 7 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 ∈ On)
73		eleq1 2848	. . . . . . . . . 10 ⊢ (𝑎 = dom 𝑇 → (𝑎 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑝))
74		suceq 6428	. . . . . . . . . . . . . 14 ⊢ (𝑎 = dom 𝑇 → suc 𝑎 = suc dom 𝑇)
75	74	reseq2d 5974	. . . . . . . . . . . . 13 ⊢ (𝑎 = dom 𝑇 → (𝑝 ↾ suc 𝑎) = (𝑝 ↾ suc dom 𝑇))
76	74	reseq2d 5974	. . . . . . . . . . . . 13 ⊢ (𝑎 = dom 𝑇 → (𝑧 ↾ suc 𝑎) = (𝑧 ↾ suc dom 𝑇))
77	75, 76	eqeq12d 2776	. . . . . . . . . . . 12 ⊢ (𝑎 = dom 𝑇 → ((𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎) ↔ (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
78	77	imbi2d 343	. . . . . . . . . . 11 ⊢ (𝑎 = dom 𝑇 → ((¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
79	78	ralbidv 3185	. . . . . . . . . 10 ⊢ (𝑎 = dom 𝑇 → (∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
80	73, 79	anbi12d 644	. . . . . . . . 9 ⊢ (𝑎 = dom 𝑇 → ((𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
81	80	rexbidv 3186	. . . . . . . 8 ⊢ (𝑎 = dom 𝑇 → (∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
82	81	elabg 3630	. . . . . . 7 ⊢ (dom 𝑇 ∈ On → (dom 𝑇 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))} ↔ ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
83	72, 82	syl 18	. . . . . 6 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → (dom 𝑇 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))} ↔ ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
84	69, 83	mpbird 260	. . . . 5 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
85	1	noinfdm 27987	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
86	85	3ad2ant1 1151	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → dom 𝑇 = {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
87	86	adantl 487	. . . . . . 7 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → dom 𝑇 = {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
88	87	adantr 486	. . . . . 6 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 = {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
89	88	eleq2d 2846	. . . . 5 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → (dom 𝑇 ∈ dom 𝑇 ↔ dom 𝑇 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))}))
90	84, 89	mpbird 260	. . . 4 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 ∈ dom 𝑇)
91	8, 90	mtand 828	. . 3 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑈‘dom 𝑇) = 2_o)
92	91	neqned 2962	. 2 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
93		rexanali 3116	. . 3 ⊢ (∃𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ↔ ¬ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o))
94		simpr1 1213	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
95		simpr2 1214	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
96		simplll 787	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧 ∈ 𝐵)
97		simpr3 1215	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
98		simpll 779	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧))
99	94, 95, 97, 98, 37	syl112anc 1401	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧 ↾ dom 𝑇) = 𝑇)
100	1	noinfbnd1lem4 27994	. . . . . . . . . . 11 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 ↾ dom 𝑇) = 𝑇)) → (𝑧‘dom 𝑇) ≠ ∅)
101	94, 95, 96, 99, 100	syl112anc 1401	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧‘dom 𝑇) ≠ ∅)
102	101	neneqd 2960	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = ∅)
103	102	pm2.21d 122	. . . . . . . 8 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ → (𝑈‘dom 𝑇) ≠ 2_o))
104	1	noinfbnd1lem3 27993	. . . . . . . . . . 11 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 ↾ dom 𝑇) = 𝑇)) → (𝑧‘dom 𝑇) ≠ 1_o)
105	94, 95, 96, 99, 104	syl112anc 1401	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧‘dom 𝑇) ≠ 1_o)
106	105	neneqd 2960	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = 1_o)
107	106	pm2.21d 122	. . . . . . . 8 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = 1_o → (𝑈‘dom 𝑇) ≠ 2_o))
108		simplr 781	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = 2_o)
109		simpr2l 1251	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝐵 ⊆ No )
110	109, 96	sseldd 3932	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧 ∈ No )
111		nofv 27925	. . . . . . . . . 10 ⊢ (𝑧 ∈ No → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1_o ∨ (𝑧‘dom 𝑇) = 2_o))
112	110, 111	syl 18	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1_o ∨ (𝑧‘dom 𝑇) = 2_o))
113		3orel3 1517	. . . . . . . . 9 ⊢ (¬ (𝑧‘dom 𝑇) = 2_o → (((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1_o ∨ (𝑧‘dom 𝑇) = 2_o) → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1_o)))
114	108, 112, 113	sylc 66	. . . . . . . 8 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1_o))
115	103, 107, 114	mpjaod 874	. . . . . . 7 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
116	115	ex 418	. . . . . 6 ⊢ (((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) → ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2_o))
117	116	anasss 472	. . . . 5 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2_o)) → ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2_o))
118	117	rexlimiva 3155	. . . 4 ⊢ (∃𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2_o) → ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2_o))
119	118	imp 412	. . 3 ⊢ ((∃𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
120	93, 119	sylanbr 594	. 2 ⊢ ((¬ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
121	92, 120	pm2.61ian 824	1 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2_o)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∨ w3o 1102 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 {cab 2738 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 ∪ cun 3897 ⊆ wss 3899 ∅c0 4279 ifcif 4482 {csn 4584 ⟨cop 4590 class class class wbr 5103 ↦ cmpt 5186 dom cdm 5655 ↾ cres 5657 Ord word 6358 Oncon0 6359 suc csuc 6361 ℩cio 6489 Fun wfun 6529 ‘cfv 6535 ℩crio 7372 1_oc1o 8455 2_oc2o 8456 No csur 27908 <s clts 27909

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7742

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-ord 6362 df-on 6363 df-suc 6365 df-iota 6491 df-fun 6537 df-fn 6538 df-f 6539 df-fo 6541 df-fv 6543 df-riota 7373 df-1o 8462 df-2o 8463 df-no 27911 df-lts 27912 df-bday 27913

This theorem is used by: noinfbnd1lem6 27996

W3C validator