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 27639

Description: Lemma for noinfbnd1 27641. 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 27630	. . . . . . . 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 27565	. . . . . 6 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
6	4, 5	syl 17	. . . . 5 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → Ord dom 𝑇)
7		ordirr 6350	. . . . 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 6893	. . . . . . . . . . 11 ⊢ (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) = ∅)
12		2on0 8448	. . . . . . . . . . . . 13 ⊢ 2_o ≠ ∅
13	12	necomi 2979	. . . . . . . . . . . 12 ⊢ ∅ ≠ 2_o
14		neeq1 2987	. . . . . . . . . . . 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 2930	. . . . . . . . 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 3947	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑈 ∈ No )
25		nofun 27561	. . . . . . . . . . . . . . 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 3947	. . . . . . . . . . . . . . 15 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → 𝑧 ∈ No )
29		nofun 27561	. . . . . . . . . . . . . . 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 27636	. . . . . . . . . . . . . . . 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 2767	. . . . . . . . . . . . . 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 6893	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) = ∅)
44		neeq1 2987	. . . . . . . . . . . . . . . . . . 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 2930	. . . . . . . . . . . . . . . 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 2767	. . . . . . . . . . . . . 14 ⊢ ((((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2_o) ∧ ((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2_o)) → (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))
51		eqfunressuc 7336	. . . . . . . . . . . . . 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 3145	. . . . . . . . 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 5867	. . . . . . . . . 10 ⊢ (𝑝 = 𝑈 → dom 𝑝 = dom 𝑈)
60	59	eleq2d 2814	. . . . . . . . 9 ⊢ (𝑝 = 𝑈 → (dom 𝑇 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑈))
61		breq1 5110	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑈 → (𝑝 <s 𝑧 ↔ 𝑈 <s 𝑧))
62	61	notbid 318	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑈 → (¬ 𝑝 <s 𝑧 ↔ ¬ 𝑈 <s 𝑧))
63		reseq1 5944	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑈 → (𝑝 ↾ suc dom 𝑇) = (𝑈 ↾ suc dom 𝑇))
64	63	eqeq1d 2731	. . . . . . . . . . 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 3156	. . . . . . . . 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 3588	. . . . . . 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 27562	. . . . . . . . 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 2816	. . . . . . . . . 10 ⊢ (𝑎 = dom 𝑇 → (𝑎 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑝))
74		suceq 6400	. . . . . . . . . . . . . 14 ⊢ (𝑎 = dom 𝑇 → suc 𝑎 = suc dom 𝑇)
75	74	reseq2d 5950	. . . . . . . . . . . . 13 ⊢ (𝑎 = dom 𝑇 → (𝑝 ↾ suc 𝑎) = (𝑝 ↾ suc dom 𝑇))
76	74	reseq2d 5950	. . . . . . . . . . . . 13 ⊢ (𝑎 = dom 𝑇 → (𝑧 ↾ suc 𝑎) = (𝑧 ↾ suc dom 𝑇))
77	75, 76	eqeq12d 2745	. . . . . . . . . . . 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 3156	. . . . . . . . . 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 3157	. . . . . . . 8 ⊢ (𝑎 = dom 𝑇 → (∃𝑝 ∈ 𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧 ∈ 𝐵 (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
82	81	elabg 3643	. . . . . . 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 27631	. . . . . . . . 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 2814	. . . . 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 2932	. 2 ⊢ ((∀𝑧 ∈ 𝐵 (¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2_o)
93		rexanali 3084	. . 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 27638	. . . . . . . . . . 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 2930	. . . . . . . . 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 27637	. . . . . . . . . . 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 2930	. . . . . . . . 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 3947	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2_o) ∧ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧 ∈ No )
111		nofv 27569	. . . . . . . . . 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 3126	. . . 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 1540 ∈ wcel 2109 {cab 2707 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 ∪ cun 3912 ⊆ wss 3914 ∅c0 4296 ifcif 4488 {csn 4589 ⟨cop 4595 class class class wbr 5107 ↦ cmpt 5188 dom cdm 5638 ↾ cres 5640 Ord word 6331 Oncon0 6332 suc csuc 6334 ℩cio 6462 Fun wfun 6505 ‘cfv 6511 ℩crio 7343 1_oc1o 8427 2_oc2o 8428 No csur 27551 <s cslt 27552

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4872 df-int 4911 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-ord 6335 df-on 6336 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-fo 6517 df-fv 6519 df-riota 7344 df-1o 8434 df-2o 8435 df-no 27554 df-slt 27555 df-bday 27556

This theorem is referenced by: noinfbnd1lem6 27640

W3C validator