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 27673

Description: Lemma for noinfbnd1 27675. 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 27664	. . . . . . . 8 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → 𝑇 ∈ No )
3	2	3ad2ant2 1131	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑇 ∈ No )
4	3	adantl 480	. . . . . 6 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑇 ∈ No )
5		nodmord 27599	. . . . . 6 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
6	4, 5	syl 17	. . . . 5 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → Ord dom 𝑇)
7		ordirr 6383	. . . . 5 ⊢ (Ord dom 𝑇 → ¬ dom 𝑇 ∈ dom 𝑇)
8	6, 7	syl 17	. . . 4 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ dom 𝑇 ∈ dom 𝑇)
9		simpr3l 1231	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑈 ∈ 𝐵)
10	9	adantr 479	. . . . . . 7 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → 𝑈 ∈ 𝐵)
11		ndmfv 6925	. . . . . . . . . . 11 ⊢ (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) = ∅)
12		2on0 8496	. . . . . . . . . . . . 13 ⊢ 2_o ≠ ∅
13	12	necomi 2985	. . . . . . . . . . . 12 ⊢ ∅ ≠ 2_o
14		neeq1 2993	. . . . . . . . . . . 12 ⊢ ((𝑈‘dom 𝑇) = ∅ → ((𝑈‘dom 𝑇) ≠ 2_o ↔ ∅ ≠ 2_o))
15	13, 14	mpbiri 257	. . . . . . . . . . 11 ⊢ ((𝑈‘dom 𝑇) = ∅ → (𝑈‘dom 𝑇) ≠ 2_o)
16	11, 15	syl 17	. . . . . . . . . 10 ⊢ (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) ≠ 2_o)
17	16	neneqd 2935	. . . . . . . . 9 ⊢ (¬ dom 𝑇 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑇) = 2_o)
18	17	con4i 114	. . . . . . . 8 ⊢ ((𝑈‘dom 𝑇) = 2_o → dom 𝑇 ∈ dom 𝑈)
19	18	adantl 480	. . . . . . 7 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 ∈ dom 𝑈)
20		simpl2l 1223	. . . . . . . . . . . . . . . . 17 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) → 𝐵 ⊆ No )
21	20	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝐵 ⊆ No )
22		simpl3l 1225	. . . . . . . . . . . . . . . . 17 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) → 𝑈 ∈ 𝐵)
23	22	adantr 479	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑈 ∈ 𝐵)
24	21, 23	sseldd 3974	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑈 ∈ No )
25		nofun 27595	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ No → Fun 𝑈)
26	24, 25	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → Fun 𝑈)
27		simprll 777	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑧 ∈ 𝐵)
28	21, 27	sseldd 3974	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑧 ∈ No )
29		nofun 27595	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ No → Fun 𝑧)
30	28, 29	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → Fun 𝑧)
31		simpl3r 1226	. . . . . . . . . . . . . . . 16 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) → (𝑈 ↾ dom 𝑇) = 𝑇)
32	31	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈 ↾ dom 𝑇) = 𝑇)
33		simpll1 1209	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
34		simpll2 1210	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
35		simpll3 1211	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
36		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧))
37	1	noinfbnd1lem2 27670	. . . . . . . . . . . . . . . 16 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ ((𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧))) → (𝑧 ↾ dom 𝑇) = 𝑇)
38	33, 34, 35, 36, 37	syl112anc 1371	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑧 ↾ dom 𝑇) = 𝑇)
39	32, 38	eqtr4d 2768	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈 ↾ dom 𝑇) = (𝑧 ↾ dom 𝑇))
40		simplr 767	. . . . . . . . . . . . . . 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 771	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑧‘dom 𝑇) = 2_o)
43		ndmfv 6925	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) = ∅)
44		neeq1 2993	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧‘dom 𝑇) = ∅ → ((𝑧‘dom 𝑇) ≠ 2_o ↔ ∅ ≠ 2_o))
45	13, 44	mpbiri 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧‘dom 𝑇) = ∅ → (𝑧‘dom 𝑇) ≠ 2_o)
46	43, 45	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) ≠ 2_o)
47	46	neneqd 2935	. . . . . . . . . . . . . . . 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 2768	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))
51		eqfunressuc 7362	. . . . . . . . . . . . . 14 ⊢ (((Fun 𝑈 ∧ Fun 𝑧) ∧ (𝑈 ↾ dom 𝑇) = (𝑧 ↾ dom 𝑇) ∧ (dom 𝑇 ∈ dom 𝑈 ∧ dom 𝑇 ∈ dom 𝑧 ∧ (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))) → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))
52	26, 30, 39, 41, 49, 50, 51	syl213anc 1386	. . . . . . . . . . . . 13 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))
53	52	expr 455	. . . . . . . . . . . 12 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ (𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧)) → ((𝑧‘dom 𝑇) = 2_o → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
54	53	expr 455	. . . . . . . . . . 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 3157	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) → (∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) → ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
57	56	impcom 406	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o)) → ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
58	57	anassrs 466	. . . . . . 7 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
59		dmeq 5901	. . . . . . . . . 10 ⊢ (𝑝 = 𝑈 → dom 𝑝 = dom 𝑈)
60	59	eleq2d 2811	. . . . . . . . 9 ⊢ (𝑝 = 𝑈 → (dom 𝑇 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑈))
61		breq1 5147	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑈 → (𝑝 <s 𝑧 ↔ 𝑈 <s 𝑧))
62	61	notbid 317	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑈 → (¬ 𝑝 <s 𝑧 ↔ ¬ 𝑈 <s 𝑧))
63		reseq1 5974	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑈 → (𝑝 ↾ suc dom 𝑇) = (𝑈 ↾ suc dom 𝑇))
64	63	eqeq1d 2727	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑈 → ((𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇) ↔ (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
65	62, 64	imbi12d 343	. . . . . . . . . 10 ⊢ (𝑝 = 𝑈 → ((¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)) ↔ (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
66	65	ralbidv 3168	. . . . . . . . 9 ⊢ (𝑝 = 𝑈 → (∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)) ↔ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
67	60, 66	anbi12d 630	. . . . . . . 8 ⊢ (𝑝 = 𝑈 → ((dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))) ↔ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
68	67	rspcev 3603	. . . . . . 7 ⊢ ((𝑈 ∈ 𝐵 ∧ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))) → ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
69	10, 19, 58, 68	syl12anc 835	. . . . . 6 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
70		nodmon 27596	. . . . . . . . 9 ⊢ (𝑇 ∈ No → dom 𝑇 ∈ On)
71	4, 70	syl 17	. . . . . . . 8 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → dom 𝑇 ∈ On)
72	71	adantr 479	. . . . . . 7 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 ∈ On)
73		eleq1 2813	. . . . . . . . . 10 ⊢ (𝑎 = dom 𝑇 → (𝑎 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑝))
74		suceq 6431	. . . . . . . . . . . . . 14 ⊢ (𝑎 = dom 𝑇 → suc 𝑎 = suc dom 𝑇)
75	74	reseq2d 5980	. . . . . . . . . . . . 13 ⊢ (𝑎 = dom 𝑇 → (𝑝 ↾ suc 𝑎) = (𝑝 ↾ suc dom 𝑇))
76	74	reseq2d 5980	. . . . . . . . . . . . 13 ⊢ (𝑎 = dom 𝑇 → (𝑧 ↾ suc 𝑎) = (𝑧 ↾ suc dom 𝑇))
77	75, 76	eqeq12d 2741	. . . . . . . . . . . 12 ⊢ (𝑎 = dom 𝑇 → ((𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎) ↔ (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
78	77	imbi2d 339	. . . . . . . . . . 11 ⊢ (𝑎 = dom 𝑇 → ((¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
79	78	ralbidv 3168	. . . . . . . . . 10 ⊢ (𝑎 = dom 𝑇 → (∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
80	73, 79	anbi12d 630	. . . . . . . . 9 ⊢ (𝑎 = dom 𝑇 → ((𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
81	80	rexbidv 3169	. . . . . . . 8 ⊢ (𝑎 = dom 𝑇 → (∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
82	81	elabg 3659	. . . . . . 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 256	. . . . 5 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
85	1	noinfdm 27665	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
86	85	3ad2ant1 1130	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → dom 𝑇 = {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
87	86	adantl 480	. . . . . . 7 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → dom 𝑇 = {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
88	87	adantr 479	. . . . . 6 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 = {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
89	88	eleq2d 2811	. . . . 5 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → (dom 𝑇 ∈ dom 𝑇 ↔ dom 𝑇 ∈ {𝑎 ∣ ∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))}))
90	84, 89	mpbird 256	. . . 4 ⊢ (((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2_o) → dom 𝑇 ∈ dom 𝑇)
91	8, 90	mtand 814	. . 3 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑈‘dom 𝑇) = 2_o)
92	91	neqned 2937	. 2 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
93		rexanali 3092	. . 3 ⊢ (∃𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ↔ ¬ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o))
94		simpr1 1191	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
95		simpr2 1192	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉))
96		simplll 773	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧 ∈ 𝐵)
97		simpr3 1193	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
98		simpll 765	. . . . . . . . . . . 12 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧))
99	94, 95, 97, 98, 37	syl112anc 1371	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧 ↾ dom 𝑇) = 𝑇)
100	1	noinfbnd1lem4 27672	. . . . . . . . . . 11 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 ↾ dom 𝑇) = 𝑇)) → (𝑧‘dom 𝑇) ≠ ∅)
101	94, 95, 96, 99, 100	syl112anc 1371	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧‘dom 𝑇) ≠ ∅)
102	101	neneqd 2935	. . . . . . . . 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 27671	. . . . . . . . . . 11 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑧 ∈ 𝐵 ∧ (𝑧 ↾ dom 𝑇) = 𝑇)) → (𝑧‘dom 𝑇) ≠ 1_o)
105	94, 95, 96, 99, 104	syl112anc 1371	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧‘dom 𝑇) ≠ 1_o)
106	105	neneqd 2935	. . . . . . . . 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 767	. . . . . . . . 9 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = 2_o)
109		simpr2l 1229	. . . . . . . . . . 11 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝐵 ⊆ No )
110	109, 96	sseldd 3974	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧 ∈ No )
111		nofv 27603	. . . . . . . . . 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 1481	. . . . . . . . 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 858	. . . . . . 7 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
116	115	ex 411	. . . . . 6 ⊢ (((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) → ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2_o))
117	116	anasss 465	. . . . 5 ⊢ ((𝑧 ∈ 𝐵 ∧ (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2_o)) → ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2_o))
118	117	rexlimiva 3137	. . . 4 ⊢ (∃𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2_o) → ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2_o))
119	118	imp 405	. . 3 ⊢ ((∃𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
120	93, 119	sylanbr 580	. 2 ⊢ ((¬ ∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
121	92, 120	pm2.61ian 810	1 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2_o)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∨ wo 845 ∨ w3o 1083 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 {cab 2702 ≠ wne 2930 ∀wral 3051 ∃wrex 3060 ∪ cun 3939 ⊆ wss 3941 ∅c0 4319 ifcif 4525 {csn 4625 ⟨cop 4631 class class class wbr 5144 ↦ cmpt 5227 dom cdm 5673 ↾ cres 5675 Ord word 6364 Oncon0 6365 suc csuc 6367 ℩cio 6493 Fun wfun 6537 ‘cfv 6543 ℩crio 7368 1_oc1o 8473 2_oc2o 8474 No csur 27586 <s cslt 27587

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 2166 ax-ext 2696 ax-rep 5281 ax-sep 5295 ax-nul 5302 ax-pr 5424 ax-un 7735

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 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 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-pss 3961 df-nul 4320 df-if 4526 df-pw 4601 df-sn 4626 df-pr 4628 df-tp 4630 df-op 4632 df-uni 4905 df-int 4946 df-iun 4994 df-br 5145 df-opab 5207 df-mpt 5228 df-tr 5262 df-id 5571 df-eprel 5577 df-po 5585 df-so 5586 df-fr 5628 df-we 5630 df-xp 5679 df-rel 5680 df-cnv 5681 df-co 5682 df-dm 5683 df-rn 5684 df-res 5685 df-ima 5686 df-ord 6368 df-on 6369 df-suc 6371 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7369 df-1o 8480 df-2o 8481 df-no 27589 df-slt 27590 df-bday 27591

This theorem is referenced by: noinfbnd1lem6 27674

W3C validator