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 27666

Description: Lemma for noinfbnd1 27668. 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 27657	. . . . . . . 8 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → 𝑇 ∈ No )
3	2	3ad2ant2 1134	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑇 ∈ No )
4	3	adantl 481	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑇 ∈ No )
5		nodmord 27592	. . . . . 6 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
6	4, 5	syl 17	. . . . 5 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → Ord dom 𝑇)
7		ordirr 6324	. . . . 5 ⊢ (Ord dom 𝑇 → ¬ dom 𝑇 ∈ dom 𝑇)
8	6, 7	syl 17	. . . 4 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ dom 𝑇 ∈ dom 𝑇)
9		simpr3l 1235	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑈 ∈ 𝐵)
10	9	adantr 480	. . . . . . 7 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → 𝑈 ∈ 𝐵)
11		ndmfv 6854	. . . . . . . . . . 11 ⊢ (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) = ∅)
12		2on0 8399	. . . . . . . . . . . . 13 ⊢ 2_o ≠ ∅
13	12	necomi 2982	. . . . . . . . . . . 12 ⊢ ∅ ≠ 2_o
14		neeq1 2990	. . . . . . . . . . . 12 ⊢ ((𝑈‘dom 𝑇) = ∅ → ((𝑈‘dom 𝑇) ≠ 2_o ↔ ∅ ≠ 2_o))
15	13, 14	mpbiri 258	. . . . . . . . . . 11 ⊢ ((𝑈‘dom 𝑇) = ∅ → (𝑈‘dom 𝑇) ≠ 2_o)
16	11, 15	syl 17	. . . . . . . . . 10 ⊢ (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) ≠ 2_o)
17	16	neneqd 2933	. . . . . . . . 9 ⊢ (¬ dom 𝑇 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑇) = 2_o)
18	17	con4i 114	. . . . . . . 8 ⊢ ((𝑈‘dom 𝑇) = 2_o → dom 𝑇 ∈ dom 𝑈)
19	18	adantl 481	. . . . . . 7 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 ∈ dom 𝑈)
20		simpl2l 1227	. . . . . . . . . . . . . . . . 17 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) → 𝐵 ⊆ No )
21	20	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝐵 ⊆ No )
22		simpl3l 1229	. . . . . . . . . . . . . . . . 17 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) → 𝑈 ∈ 𝐵)
23	22	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑈 ∈ 𝐵)
24	21, 23	sseldd 3930	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑈 ∈ No )
25		nofun 27588	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ No → Fun 𝑈)
26	24, 25	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → Fun 𝑈)
27		simprll 778	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑧 ∈ 𝐵)
28	21, 27	sseldd 3930	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑧 ∈ No )
29		nofun 27588	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ No → Fun 𝑧)
30	28, 29	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → Fun 𝑧)
31		simpl3r 1230	. . . . . . . . . . . . . . . 16 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) → (𝑈 ↾ dom 𝑇) = 𝑇)
32	31	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈 ↾ dom 𝑇) = 𝑇)
33		simpll1 1213	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
34		simpll2 1214	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
35		simpll3 1215	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
36		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧))
37	1	noinfbnd1lem2 27663	. . . . . . . . . . . . . . . 16 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ ((𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧))) → (𝑧 ↾ dom 𝑇) = 𝑇)
38	33, 34, 35, 36, 37	syl112anc 1376	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑧 ↾ dom 𝑇) = 𝑇)
39	32, 38	eqtr4d 2769	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈 ↾ dom 𝑇) = (𝑧 ↾ dom 𝑇))
40		simplr 768	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈‘dom 𝑇) = 2_o)
41	40, 18	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → dom 𝑇 ∈ dom 𝑈)
42		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑧‘dom 𝑇) = 2_o)
43		ndmfv 6854	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) = ∅)
44		neeq1 2990	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧‘dom 𝑇) = ∅ → ((𝑧‘dom 𝑇) ≠ 2_o ↔ ∅ ≠ 2_o))
45	13, 44	mpbiri 258	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧‘dom 𝑇) = ∅ → (𝑧‘dom 𝑇) ≠ 2_o)
46	43, 45	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) ≠ 2_o)
47	46	neneqd 2933	. . . . . . . . . . . . . . . 16 ⊢ (¬ dom 𝑇 ∈ dom 𝑧 → ¬ (𝑧‘dom 𝑇) = 2_o)
48	47	con4i 114	. . . . . . . . . . . . . . 15 ⊢ ((𝑧‘dom 𝑇) = 2_o → dom 𝑇 ∈ dom 𝑧)
49	42, 48	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → dom 𝑇 ∈ dom 𝑧)
50	40, 42	eqtr4d 2769	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))
51		eqfunressuc 7295	. . . . . . . . . . . . . 14 ⊢ (((Fun 𝑈 ∧ Fun 𝑧) ∧ (𝑈 ↾ dom 𝑇) = (𝑧 ↾ dom 𝑇) ∧ (dom 𝑇 ∈ dom 𝑈 ∧ dom 𝑇 ∈ dom 𝑧 ∧ (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))) → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))
52	26, 30, 39, 41, 49, 50, 51	syl213anc 1391	. . . . . . . . . . . . 13 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))
53	52	expr 456	. . . . . . . . . . . 12 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧)) → ((𝑧‘dom 𝑇) = 2_o → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
54	53	expr 456	. . . . . . . . . . 11 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ 𝑧 ∈ 𝐵) → (¬ 𝑈 <s 𝑧 → ((𝑧‘dom 𝑇) = 2_o → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
55	54	a2d 29	. . . . . . . . . 10 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ 𝑧 ∈ 𝐵) → ((¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) → (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
56	55	ralimdva 3144	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) → (∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) → ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
57	56	impcom 407	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o)) → ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
58	57	anassrs 467	. . . . . . 7 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
59		dmeq 5842	. . . . . . . . . 10 ⊢ (𝑝 = 𝑈 → dom 𝑝 = dom 𝑈)
60	59	eleq2d 2817	. . . . . . . . 9 ⊢ (𝑝 = 𝑈 → (dom 𝑇 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑈))
61		breq1 5092	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑈 → (𝑝 <s 𝑧 ↔ 𝑈 <s 𝑧))
62	61	notbid 318	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑈 → (¬ 𝑝 <s 𝑧 ↔ ¬ 𝑈 <s 𝑧))
63		reseq1 5921	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑈 → (𝑝 ↾ suc dom 𝑇) = (𝑈 ↾ suc dom 𝑇))
64	63	eqeq1d 2733	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑈 → ((𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇) ↔ (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
65	62, 64	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑝 = 𝑈 → ((¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)) ↔ (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
66	65	ralbidv 3155	. . . . . . . . 9 ⊢ (𝑝 = 𝑈 → (∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)) ↔ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
67	60, 66	anbi12d 632	. . . . . . . 8 ⊢ (𝑝 = 𝑈 → ((dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))) ↔ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
68	67	rspcev 3572	. . . . . . 7 ⊢ ((𝑈 ∈ 𝐵 ∧ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))) → ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
69	10, 19, 58, 68	syl12anc 836	. . . . . 6 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
70		nodmon 27589	. . . . . . . . 9 ⊢ (𝑇 ∈ No → dom 𝑇 ∈ On)
71	4, 70	syl 17	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → dom 𝑇 ∈ On)
72	71	adantr 480	. . . . . . 7 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 ∈ On)
73		eleq1 2819	. . . . . . . . . 10 ⊢ (𝑎 = dom 𝑇 → (𝑎 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑝))
74		suceq 6374	. . . . . . . . . . . . . 14 ⊢ (𝑎 = dom 𝑇 → suc 𝑎 = suc dom 𝑇)
75	74	reseq2d 5927	. . . . . . . . . . . . 13 ⊢ (𝑎 = dom 𝑇 → (𝑝 ↾ suc 𝑎) = (𝑝 ↾ suc dom 𝑇))
76	74	reseq2d 5927	. . . . . . . . . . . . 13 ⊢ (𝑎 = dom 𝑇 → (𝑧 ↾ suc 𝑎) = (𝑧 ↾ suc dom 𝑇))
77	75, 76	eqeq12d 2747	. . . . . . . . . . . 12 ⊢ (𝑎 = dom 𝑇 → ((𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎) ↔ (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
78	77	imbi2d 340	. . . . . . . . . . 11 ⊢ (𝑎 = dom 𝑇 → ((¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
79	78	ralbidv 3155	. . . . . . . . . 10 ⊢ (𝑎 = dom 𝑇 → (∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
80	73, 79	anbi12d 632	. . . . . . . . 9 ⊢ (𝑎 = dom 𝑇 → ((𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
81	80	rexbidv 3156	. . . . . . . 8 ⊢ (𝑎 = dom 𝑇 → (∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
82	81	elabg 3627	. . . . . . 7 ⊢ (dom 𝑇 ∈ On → (dom 𝑇 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))} ↔ ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
83	72, 82	syl 17	. . . . . 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 257	. . . . 5 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
85	1	noinfdm 27658	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
86	85	3ad2ant1 1133	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → dom 𝑇 = {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
87	86	adantl 481	. . . . . . 7 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → dom 𝑇 = {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
88	87	adantr 480	. . . . . 6 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 = {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
89	88	eleq2d 2817	. . . . 5 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → (dom 𝑇 ∈ dom 𝑇 ↔ dom 𝑇 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))}))
90	84, 89	mpbird 257	. . . 4 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 ∈ dom 𝑇)
91	8, 90	mtand 815	. . 3 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑈‘dom 𝑇) = 2_o)
92	91	neqned 2935	. 2 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
93		rexanali 3086	. . 3 ⊢ (∃𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ↔ ¬ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o))
94		simpr1 1195	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
95		simpr2 1196	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
96		simplll 774	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧 ∈ 𝐵)
97		simpr3 1197	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
98		simpll 766	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧))
99	94, 95, 97, 98, 37	syl112anc 1376	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧 ↾ dom 𝑇) = 𝑇)
100	1	noinfbnd1lem4 27665	. . . . . . . . . . 11 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 ↾ dom 𝑇) = 𝑇)) → (𝑧‘dom 𝑇) ≠ ∅)
101	94, 95, 96, 99, 100	syl112anc 1376	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧‘dom 𝑇) ≠ ∅)
102	101	neneqd 2933	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = ∅)
103	102	pm2.21d 121	. . . . . . . 8 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ → (𝑈‘dom 𝑇) ≠ 2_o))
104	1	noinfbnd1lem3 27664	. . . . . . . . . . 11 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 ↾ dom 𝑇) = 𝑇)) → (𝑧‘dom 𝑇) ≠ 1_o)
105	94, 95, 96, 99, 104	syl112anc 1376	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧‘dom 𝑇) ≠ 1_o)
106	105	neneqd 2933	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = 1_o)
107	106	pm2.21d 121	. . . . . . . 8 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = 1_o → (𝑈‘dom 𝑇) ≠ 2_o))
108		simplr 768	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = 2_o)
109		simpr2l 1233	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝐵 ⊆ No )
110	109, 96	sseldd 3930	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧 ∈ No )
111		nofv 27596	. . . . . . . . . 10 ⊢ (𝑧 ∈ No → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1_o ∨ (𝑧‘dom 𝑇) = 2_o))
112	110, 111	syl 17	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1_o ∨ (𝑧‘dom 𝑇) = 2_o))
113		3orel3 1488	. . . . . . . . 9 ⊢ (¬ (𝑧‘dom 𝑇) = 2_o → (((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1_o ∨ (𝑧‘dom 𝑇) = 2_o) → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1_o)))
114	108, 112, 113	sylc 65	. . . . . . . 8 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1_o))
115	103, 107, 114	mpjaod 860	. . . . . . 7 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
116	115	ex 412	. . . . . 6 ⊢ (((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) → ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2_o))
117	116	anasss 466	. . . . 5 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2_o)) → ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2_o))
118	117	rexlimiva 3125	. . . 4 ⊢ (∃𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2_o) → ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2_o))
119	118	imp 406	. . 3 ⊢ ((∃𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
120	93, 119	sylanbr 582	. 2 ⊢ ((¬ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
121	92, 120	pm2.61ian 811	1 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2_o)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∨ w3o 1085 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 {cab 2709 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 ∪ cun 3895 ⊆ wss 3897 ∅c0 4280 ifcif 4472 {csn 4573 ⟨cop 4579 class class class wbr 5089 ↦ cmpt 5170 dom cdm 5614 ↾ cres 5616 Ord word 6305 Oncon0 6306 suc csuc 6308 ℩cio 6435 Fun wfun 6475 ‘cfv 6481 ℩crio 7302 1_oc1o 8378 2_oc2o 8379 No csur 27578 <s cslt 27579

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-tp 4578 df-op 4580 df-uni 4857 df-int 4896 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-ord 6309 df-on 6310 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-fo 6487 df-fv 6489 df-riota 7303 df-1o 8385 df-2o 8386 df-no 27581 df-slt 27582 df-bday 27583

This theorem is referenced by: noinfbnd1lem6 27667

W3C validator