noinfbnd2 - Metamath Proof Explorer

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

Theorem noinfbnd2 27895

Description: Bounding law from below for the surreal infimum. Analagous to proposition 4.3 of [Lipparini] p. 6. (Contributed by Scott Fenton, 9-Aug-2024.)

**Hypothesis**
Ref	Expression
noinfbnd2.1	⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))

**Assertion**
Ref	Expression
noinfbnd2	⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) → (∀𝑏 ∈ 𝐵 𝑍 <s 𝑏 ↔ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))

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

Proof of Theorem noinfbnd2 Dummy variables 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1944	. . . . . 6 ⊢ Ⅎ𝑥((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)
2		noinfbnd2.1	. . . . . . . . 9 ⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
3		nfre1 3290	. . . . . . . . . 10 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥
4		nfriota1 7374	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
5	4	nfdm 5941	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
6		nfcv 2925	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥1_o
7	5, 6	nfop 4854	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩
8	7	nfsn 4673	. . . . . . . . . . 11 ⊢ Ⅎ𝑥{⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}
9	4, 8	nfun 4124	. . . . . . . . . 10 ⊢ Ⅎ𝑥((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩})
10		nfcv 2925	. . . . . . . . . . 11 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
11		nfiota1 6494	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
12	10, 11	nfmpt 5209	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
13	3, 9, 12	nfif 4518	. . . . . . . . 9 ⊢ Ⅎ𝑥if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
14	2, 13	nfcxfr 2923	. . . . . . . 8 ⊢ Ⅎ𝑥𝑇
15		nfcv 2925	. . . . . . . 8 ⊢ Ⅎ𝑥 <s
16		nfcv 2925	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑍
17	14	nfdm 5941	. . . . . . . . 9 ⊢ Ⅎ𝑥dom 𝑇
18	16, 17	nfres 5980	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑍 ↾ dom 𝑇)
19	14, 15, 18	nfbr 5158	. . . . . . 7 ⊢ Ⅎ𝑥 𝑇 <s (𝑍 ↾ dom 𝑇)
20	19	nfn 1887	. . . . . 6 ⊢ Ⅎ𝑥 ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)
21	1, 20	nfim 1926	. . . . 5 ⊢ Ⅎ𝑥(((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
22		noinfbnd2lem1 27894	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑥))
23	22	3expb 1138	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ¬ (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑥))
24		rspe 3255	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
25	24	adantr 485	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
26	25	iftrued 4495	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}))
27		simpl 487	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥))
28		simprl1 1237	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → 𝐵 ⊆ No )
29		nominmo 27863	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ⊆ No → ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
30	28, 29	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
31		reu5 3371	. . . . . . . . . . . . . 14 ⊢ (∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥))
32	25, 30, 31	sylanbrc 594	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
33		riota1 7388	. . . . . . . . . . . . 13 ⊢ (∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ↔ (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
34	32, 33	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ↔ (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
35	27, 34	mpbid 235	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) = 𝑥)
36	35	dmeqd 5895	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) = dom 𝑥)
37	36	opeq1d 4844	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩ = ⟨dom 𝑥, 1_o⟩)
38	37	sneqd 4601	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩} = {⟨dom 𝑥, 1_o⟩})
39	35, 38	uneq12d 4123	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}) = (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}))
40	26, 39	eqtrd 2798	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}))
41	2, 40	eqtrid 2810	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → 𝑇 = (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}))
42	41	dmeqd 5895	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → dom 𝑇 = dom (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}))
43		1oex 8459	. . . . . . . . . . . . 13 ⊢ 1_o ∈ V
44	43	dmsnop 6217	. . . . . . . . . . . 12 ⊢ dom {⟨dom 𝑥, 1_o⟩} = {dom 𝑥}
45	44	uneq2i 4119	. . . . . . . . . . 11 ⊢ (dom 𝑥 ∪ dom {⟨dom 𝑥, 1_o⟩}) = (dom 𝑥 ∪ {dom 𝑥})
46		dmun 5900	. . . . . . . . . . 11 ⊢ dom (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 1_o⟩})
47		df-suc 6366	. . . . . . . . . . 11 ⊢ suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
48	45, 46, 47	3eqtr4ri 2797	. . . . . . . . . 10 ⊢ suc dom 𝑥 = dom (𝑥 ∪ {⟨dom 𝑥, 1_o⟩})
49	42, 48	eqtr4di 2816	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → dom 𝑇 = suc dom 𝑥)
50	49	reseq2d 5978	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑍 ↾ dom 𝑇) = (𝑍 ↾ suc dom 𝑥))
51	41, 50	breq12d 5122	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑇 <s (𝑍 ↾ dom 𝑇) ↔ (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑥)))
52	23, 51	mtbird 328	. . . . . 6 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
53	52	exp31 424	. . . . 5 ⊢ (𝑥 ∈ 𝐵 → (∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))))
54	21, 53	rexlimi 3265	. . . 4 ⊢ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))
55	54	imp 411	. . 3 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
56		simprl3 1239	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → 𝑍 ∈ No )
57	2	noinfno 27882	. . . . . . . . 9 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → 𝑇 ∈ No )
58	57	3adant3 1150	. . . . . . . 8 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) → 𝑇 ∈ No )
59	58	ad2antrl 740	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → 𝑇 ∈ No )
60		nodmon 27814	. . . . . . 7 ⊢ (𝑇 ∈ No → dom 𝑇 ∈ On)
61	59, 60	syl 18	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → dom 𝑇 ∈ On)
62		noreson 27824	. . . . . 6 ⊢ ((𝑍 ∈ No ∧ dom 𝑇 ∈ On) → (𝑍 ↾ dom 𝑇) ∈ No )
63	56, 61, 62	syl2anc 595	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑍 ↾ dom 𝑇) ∈ No )
64		nofun 27813	. . . . . . . . 9 ⊢ (𝑇 ∈ No → Fun 𝑇)
65		funrel 6553	. . . . . . . . 9 ⊢ (Fun 𝑇 → Rel 𝑇)
66	58, 64, 65	3syl 19	. . . . . . . 8 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) → Rel 𝑇)
67	66	ad2antrl 740	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → Rel 𝑇)
68		resdm 6025	. . . . . . 7 ⊢ (Rel 𝑇 → (𝑇 ↾ dom 𝑇) = 𝑇)
69	67, 68	syl 18	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑇 ↾ dom 𝑇) = 𝑇)
70	69, 59	eqeltrd 2863	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑇 ↾ dom 𝑇) ∈ No )
71		resdmss 6236	. . . . . 6 ⊢ dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇
72	71	a1i 11	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇)
73		resdmss 6236	. . . . . 6 ⊢ dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇
74	73	a1i 11	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇)
75	2	noinfdm 27883	. . . . . . . . . . 11 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑔 ∣ ∃𝑝 ∈ 𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))})
76	75	eqabrd 2904	. . . . . . . . . 10 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (𝑔 ∈ dom 𝑇 ↔ ∃𝑝 ∈ 𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
77	76	adantr 485	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 ↔ ∃𝑝 ∈ 𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
78		simpll 778	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
79		simprl1 1237	. . . . . . . . . . . . 13 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → 𝐵 ⊆ No )
80	79	adantr 485	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐵 ⊆ No )
81		simprl2 1238	. . . . . . . . . . . . 13 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → 𝐵 ∈ 𝑉)
82	81	adantr 485	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐵 ∈ 𝑉)
83		simprl 782	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 ∈ 𝐵)
84		simprrl 792	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ dom 𝑝)
85		simprrr 793	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
86		breq2 5113	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = 𝑣 → (𝑝 <s 𝑞 ↔ 𝑝 <s 𝑣))
87	86	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑣 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣))
88		reseq1 5972	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = 𝑣 → (𝑞 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))
89	88	eqeq2d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑣 → ((𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔) ↔ (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
90	87, 89	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑣 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
91	90	cbvralvw 3243	. . . . . . . . . . . . 13 ⊢ (∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
92	85, 91	sylib 221	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
93	2	noinfres 27886	. . . . . . . . . . . 12 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑝 ∈ 𝐵 ∧ 𝑔 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (𝑇 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔))
94	78, 80, 82, 83, 84, 92, 93	syl123anc 1414	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝑇 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔))
95		breq2 5113	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑝 → (𝑍 <s 𝑏 ↔ 𝑍 <s 𝑝))
96		simplrr 789	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)
97	95, 96, 83	rspcdva 3582	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 <s 𝑝)
98	56	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 ∈ No )
99	80, 83	sseldd 3938	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 ∈ No )
100		ltsso 27840	. . . . . . . . . . . . . . 15 ⊢ <s Or No
101		soasym 5602	. . . . . . . . . . . . . . 15 ⊢ (( <s Or No ∧ (𝑍 ∈ No ∧ 𝑝 ∈ No )) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
102	100, 101	mpan 702	. . . . . . . . . . . . . 14 ⊢ ((𝑍 ∈ No ∧ 𝑝 ∈ No ) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
103	98, 99, 102	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
104	97, 103	mpd 16	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ 𝑝 <s 𝑍)
105		nodmon 27814	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ No → dom 𝑝 ∈ On)
106	99, 105	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → dom 𝑝 ∈ On)
107		onelon 6385	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝑝 ∈ On ∧ 𝑔 ∈ dom 𝑝) → 𝑔 ∈ On)
108	106, 84, 107	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ On)
109		onsucb 7809	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ On ↔ suc 𝑔 ∈ On)
110	108, 109	sylib 221	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → suc 𝑔 ∈ On)
111		ltsres 27826	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ No ∧ 𝑍 ∈ No ∧ suc 𝑔 ∈ On) → ((𝑝 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔) → 𝑝 <s 𝑍))
112	99, 98, 110, 111	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ((𝑝 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔) → 𝑝 <s 𝑍))
113	104, 112	mtod 201	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑝 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
114	94, 113	eqnbrtrd 5129	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
115	114	rexlimdvaa 3167	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (∃𝑝 ∈ 𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
116	77, 115	sylbid 243	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
117	116	imp 411	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
118		nodmord 27817	. . . . . . . . . . 11 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
119		ordsucss 7810	. . . . . . . . . . 11 ⊢ (Ord dom 𝑇 → (𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇))
120	59, 118, 119	3syl 19	. . . . . . . . . 10 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇))
121	120	imp 411	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → suc 𝑔 ⊆ dom 𝑇)
122	121	resabs1d 6007	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) = (𝑇 ↾ suc 𝑔))
123	121	resabs1d 6007	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔) = (𝑍 ↾ suc 𝑔))
124	122, 123	breq12d 5122	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → (((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔) ↔ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
125	117, 124	mtbird 328	. . . . . 6 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ¬ ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔))
126	125	ralrimiva 3157	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ∀𝑔 ∈ dom 𝑇 ¬ ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔))
127		noresle 27861	. . . . 5 ⊢ ((((𝑍 ↾ dom 𝑇) ∈ No ∧ (𝑇 ↾ dom 𝑇) ∈ No ) ∧ (dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇 ∧ dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇 ∧ ∀𝑔 ∈ dom 𝑇 ¬ ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔))) → ¬ (𝑇 ↾ dom 𝑇) <s (𝑍 ↾ dom 𝑇))
128	63, 70, 72, 74, 126, 127	syl23anc 1404	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ¬ (𝑇 ↾ dom 𝑇) <s (𝑍 ↾ dom 𝑇))
129	69	breq1d 5119	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ((𝑇 ↾ dom 𝑇) <s (𝑍 ↾ dom 𝑇) ↔ 𝑇 <s (𝑍 ↾ dom 𝑇)))
130	128, 129	mtbid 327	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
131	55, 130	pm2.61ian 823	. 2 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
132		simplr 780	. . . . 5 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
133		simpll1 1231	. . . . . 6 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝐵 ⊆ No )
134		simpll2 1232	. . . . . 6 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝐵 ∈ 𝑉)
135		simpr 489	. . . . . 6 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
136	2	noinfbnd1 27893	. . . . . 6 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) → 𝑇 <s (𝑏 ↾ dom 𝑇))
137	133, 134, 135, 136	syl3anc 1398	. . . . 5 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝑇 <s (𝑏 ↾ dom 𝑇))
138		simpl3 1212	. . . . . . . 8 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝑍 ∈ No )
139		simpl1 1210	. . . . . . . . . 10 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝐵 ⊆ No )
140		simpl2 1211	. . . . . . . . . 10 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝐵 ∈ 𝑉)
141	139, 140, 57	syl2anc 595	. . . . . . . . 9 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝑇 ∈ No )
142	141, 60	syl 18	. . . . . . . 8 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → dom 𝑇 ∈ On)
143	138, 142, 62	syl2anc 595	. . . . . . 7 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) ∈ No )
144	143	adantr 485	. . . . . 6 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → (𝑍 ↾ dom 𝑇) ∈ No )
145	141	adantr 485	. . . . . 6 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝑇 ∈ No )
146	139	sselda 3937	. . . . . . 7 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No )
147	142	adantr 485	. . . . . . 7 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → dom 𝑇 ∈ On)
148		noreson 27824	. . . . . . 7 ⊢ ((𝑏 ∈ No ∧ dom 𝑇 ∈ On) → (𝑏 ↾ dom 𝑇) ∈ No )
149	146, 147, 148	syl2anc 595	. . . . . 6 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ dom 𝑇) ∈ No )
150		sotr2 5603	. . . . . . 7 ⊢ (( <s Or No ∧ ((𝑍 ↾ dom 𝑇) ∈ No ∧ 𝑇 ∈ No ∧ (𝑏 ↾ dom 𝑇) ∈ No )) → ((¬ 𝑇 <s (𝑍 ↾ dom 𝑇) ∧ 𝑇 <s (𝑏 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇)))
151	100, 150	mpan 702	. . . . . 6 ⊢ (((𝑍 ↾ dom 𝑇) ∈ No ∧ 𝑇 ∈ No ∧ (𝑏 ↾ dom 𝑇) ∈ No ) → ((¬ 𝑇 <s (𝑍 ↾ dom 𝑇) ∧ 𝑇 <s (𝑏 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇)))
152	144, 145, 149, 151	syl3anc 1398	. . . . 5 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → ((¬ 𝑇 <s (𝑍 ↾ dom 𝑇) ∧ 𝑇 <s (𝑏 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇)))
153	132, 137, 152	mp2and 711	. . . 4 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇))
154		simpll3 1233	. . . . 5 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝑍 ∈ No )
155		ltsres 27826	. . . . 5 ⊢ ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ dom 𝑇 ∈ On) → ((𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇) → 𝑍 <s 𝑏))
156	154, 146, 147, 155	syl3anc 1398	. . . 4 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → ((𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇) → 𝑍 <s 𝑏))
157	153, 156	mpd 16	. . 3 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝑍 <s 𝑏)
158	157	ralrimiva 3157	. 2 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)
159	131, 158	impbida 812	1 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) → (∀𝑏 ∈ 𝐵 𝑍 <s 𝑏 ↔ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 {cab 2741 ∀wral 3079 ∃wrex 3089 ∃!wreu 3367 ∃*wrmo 3368 ∪ cun 3903 ⊆ wss 3905 ifcif 4487 {csn 4589 ⟨cop 4595 class class class wbr 5109 ↦ cmpt 5192 Or wor 5568 dom cdm 5661 ↾ cres 5663 Rel wrel 5666 Ord word 6359 Oncon0 6360 suc csuc 6362 ℩cio 6490 Fun wfun 6530 ‘cfv 6536 ℩crio 7366 1_oc1o 8442 No csur 27804 <s clts 27805

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-int 4913 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-ord 6363 df-on 6364 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-1o 8449 df-2o 8450 df-no 27807 df-lts 27808 df-bday 27809

This theorem is referenced by: nosupinfsep 27896 noetainflem4 27904

W3C validator