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 27711

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 1916	. . . . . 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 3263	. . . . . . . . . 10 ⊢ Ⅎ𝑥∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥
4		nfriota1 7332	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
5	4	nfdm 5908	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
6		nfcv 2899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥1_o
7	5, 6	nfop 4847	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩
8	7	nfsn 4666	. . . . . . . . . . 11 ⊢ Ⅎ𝑥{⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}
9	4, 8	nfun 4124	. . . . . . . . . 10 ⊢ Ⅎ𝑥((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩})
10		nfcv 2899	. . . . . . . . . . 11 ⊢ Ⅎ𝑥{𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
11		nfiota1 6458	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))
12	10, 11	nfmpt 5198	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
13	3, 9, 12	nfif 4512	. . . . . . . . 9 ⊢ Ⅎ𝑥if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
14	2, 13	nfcxfr 2897	. . . . . . . 8 ⊢ Ⅎ𝑥𝑇
15		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑥 <s
16		nfcv 2899	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑍
17	14	nfdm 5908	. . . . . . . . 9 ⊢ Ⅎ𝑥dom 𝑇
18	16, 17	nfres 5948	. . . . . . . 8 ⊢ Ⅎ𝑥(𝑍 ↾ dom 𝑇)
19	14, 15, 18	nfbr 5147	. . . . . . 7 ⊢ Ⅎ𝑥 𝑇 <s (𝑍 ↾ dom 𝑇)
20	19	nfn 1859	. . . . . 6 ⊢ Ⅎ𝑥 ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)
21	1, 20	nfim 1898	. . . . 5 ⊢ Ⅎ𝑥(((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
22		noinfbnd2lem1 27710	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑥))
23	22	3expb 1121	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ¬ (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑥))
24		rspe 3228	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
25	24	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
26	25	iftrued 4489	. . . . . . . . . 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 482	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥))
28		simprl1 1220	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → 𝐵 ⊆ No )
29		nominmo 27679	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ⊆ No → ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
30	28, 29	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
31		reu5 3354	. . . . . . . . . . . . . 14 ⊢ (∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥))
32	25, 30, 31	sylanbrc 584	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
33		riota1 7346	. . . . . . . . . . . . 13 ⊢ (∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ↔ (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
34	32, 33	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ↔ (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) = 𝑥))
35	27, 34	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) = 𝑥)
36	35	dmeqd 5862	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) = dom 𝑥)
37	36	opeq1d 4837	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ⟨dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1_o⟩ = ⟨dom 𝑥, 1_o⟩)
38	37	sneqd 4594	. . . . . . . . . . 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 2772	. . . . . . . . 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 2784	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → 𝑇 = (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}))
42	41	dmeqd 5862	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → dom 𝑇 = dom (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}))
43		1oex 8417	. . . . . . . . . . . . 13 ⊢ 1_o ∈ V
44	43	dmsnop 6182	. . . . . . . . . . . 12 ⊢ dom {⟨dom 𝑥, 1_o⟩} = {dom 𝑥}
45	44	uneq2i 4119	. . . . . . . . . . 11 ⊢ (dom 𝑥 ∪ dom {⟨dom 𝑥, 1_o⟩}) = (dom 𝑥 ∪ {dom 𝑥})
46		dmun 5867	. . . . . . . . . . 11 ⊢ dom (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}) = (dom 𝑥 ∪ dom {⟨dom 𝑥, 1_o⟩})
47		df-suc 6331	. . . . . . . . . . 11 ⊢ suc dom 𝑥 = (dom 𝑥 ∪ {dom 𝑥})
48	45, 46, 47	3eqtr4ri 2771	. . . . . . . . . 10 ⊢ suc dom 𝑥 = dom (𝑥 ∪ {⟨dom 𝑥, 1_o⟩})
49	42, 48	eqtr4di 2790	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → dom 𝑇 = suc dom 𝑥)
50	49	reseq2d 5946	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑍 ↾ dom 𝑇) = (𝑍 ↾ suc dom 𝑥))
51	41, 50	breq12d 5113	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑇 <s (𝑍 ↾ dom 𝑇) ↔ (𝑥 ∪ {⟨dom 𝑥, 1_o⟩}) <s (𝑍 ↾ suc dom 𝑥)))
52	23, 51	mtbird 325	. . . . . 6 ⊢ (((𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
53	52	exp31 419	. . . . 5 ⊢ (𝑥 ∈ 𝐵 → (∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))))
54	21, 53	rexlimi 3238	. . . 4 ⊢ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))
55	54	imp 406	. . 3 ⊢ ((∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
56		simprl3 1222	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → 𝑍 ∈ No )
57	2	noinfno 27698	. . . . . . . . 9 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) → 𝑇 ∈ No )
58	57	3adant3 1133	. . . . . . . 8 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) → 𝑇 ∈ No )
59	58	ad2antrl 729	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → 𝑇 ∈ No )
60		nodmon 27630	. . . . . . 7 ⊢ (𝑇 ∈ No → dom 𝑇 ∈ On)
61	59, 60	syl 17	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → dom 𝑇 ∈ On)
62		noreson 27640	. . . . . 6 ⊢ ((𝑍 ∈ No ∧ dom 𝑇 ∈ On) → (𝑍 ↾ dom 𝑇) ∈ No )
63	56, 61, 62	syl2anc 585	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑍 ↾ dom 𝑇) ∈ No )
64		nofun 27629	. . . . . . . . 9 ⊢ (𝑇 ∈ No → Fun 𝑇)
65		funrel 6517	. . . . . . . . 9 ⊢ (Fun 𝑇 → Rel 𝑇)
66	58, 64, 65	3syl 18	. . . . . . . 8 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) → Rel 𝑇)
67	66	ad2antrl 729	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → Rel 𝑇)
68		resdm 5993	. . . . . . 7 ⊢ (Rel 𝑇 → (𝑇 ↾ dom 𝑇) = 𝑇)
69	67, 68	syl 17	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑇 ↾ dom 𝑇) = 𝑇)
70	69, 59	eqeltrd 2837	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑇 ↾ dom 𝑇) ∈ No )
71		resdmss 6201	. . . . . 6 ⊢ dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇
72	71	a1i 11	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → dom (𝑍 ↾ dom 𝑇) ⊆ dom 𝑇)
73		resdmss 6201	. . . . . 6 ⊢ dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇
74	73	a1i 11	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → dom (𝑇 ↾ dom 𝑇) ⊆ dom 𝑇)
75	2	noinfdm 27699	. . . . . . . . . . 11 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑔 ∣ ∃𝑝 ∈ 𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))})
76	75	eqabrd 2878	. . . . . . . . . 10 ⊢ (¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (𝑔 ∈ dom 𝑇 ↔ ∃𝑝 ∈ 𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
77	76	adantr 480	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 ↔ ∃𝑝 ∈ 𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
78		simpll 767	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)
79		simprl1 1220	. . . . . . . . . . . . 13 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → 𝐵 ⊆ No )
80	79	adantr 480	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐵 ⊆ No )
81		simprl2 1221	. . . . . . . . . . . . 13 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → 𝐵 ∈ 𝑉)
82	81	adantr 480	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐵 ∈ 𝑉)
83		simprl 771	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 ∈ 𝐵)
84		simprrl 781	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ dom 𝑝)
85		simprrr 782	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
86		breq2 5104	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = 𝑣 → (𝑝 <s 𝑞 ↔ 𝑝 <s 𝑣))
87	86	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑣 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣))
88		reseq1 5940	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = 𝑣 → (𝑞 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))
89	88	eqeq2d 2748	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑣 → ((𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔) ↔ (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
90	87, 89	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑣 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
91	90	cbvralvw 3216	. . . . . . . . . . . . 13 ⊢ (∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
92	85, 91	sylib 218	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
93	2	noinfres 27702	. . . . . . . . . . . 12 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉) ∧ (𝑝 ∈ 𝐵 ∧ 𝑔 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (𝑇 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔))
94	78, 80, 82, 83, 84, 92, 93	syl123anc 1390	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝑇 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔))
95		breq2 5104	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑝 → (𝑍 <s 𝑏 ↔ 𝑍 <s 𝑝))
96		simplrr 778	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)
97	95, 96, 83	rspcdva 3579	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 <s 𝑝)
98	56	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 ∈ No )
99	80, 83	sseldd 3936	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 ∈ No )
100		ltsso 27656	. . . . . . . . . . . . . . 15 ⊢ <s Or No
101		soasym 5573	. . . . . . . . . . . . . . 15 ⊢ (( <s Or No ∧ (𝑍 ∈ No ∧ 𝑝 ∈ No )) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
102	100, 101	mpan 691	. . . . . . . . . . . . . 14 ⊢ ((𝑍 ∈ No ∧ 𝑝 ∈ No ) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
103	98, 99, 102	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝑍 <s 𝑝 → ¬ 𝑝 <s 𝑍))
104	97, 103	mpd 15	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ 𝑝 <s 𝑍)
105		nodmon 27630	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ∈ No → dom 𝑝 ∈ On)
106	99, 105	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → dom 𝑝 ∈ On)
107		onelon 6350	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝑝 ∈ On ∧ 𝑔 ∈ dom 𝑝) → 𝑔 ∈ On)
108	106, 84, 107	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ On)
109		onsucb 7769	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ On ↔ suc 𝑔 ∈ On)
110	108, 109	sylib 218	. . . . . . . . . . . . 13 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → suc 𝑔 ∈ On)
111		ltsres 27642	. . . . . . . . . . . . 13 ⊢ ((𝑝 ∈ No ∧ 𝑍 ∈ No ∧ suc 𝑔 ∈ On) → ((𝑝 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔) → 𝑝 <s 𝑍))
112	99, 98, 110, 111	syl3anc 1374	. . . . . . . . . . . 12 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ((𝑝 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔) → 𝑝 <s 𝑍))
113	104, 112	mtod 198	. . . . . . . . . . 11 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑝 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
114	94, 113	eqnbrtrd 5118	. . . . . . . . . 10 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ (𝑝 ∈ 𝐵 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
115	114	rexlimdvaa 3140	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (∃𝑝 ∈ 𝐵 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
116	77, 115	sylbid 240	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
117	116	imp 406	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ¬ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔))
118		nodmord 27633	. . . . . . . . . . 11 ⊢ (𝑇 ∈ No → Ord dom 𝑇)
119		ordsucss 7770	. . . . . . . . . . 11 ⊢ (Ord dom 𝑇 → (𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇))
120	59, 118, 119	3syl 18	. . . . . . . . . 10 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → (𝑔 ∈ dom 𝑇 → suc 𝑔 ⊆ dom 𝑇))
121	120	imp 406	. . . . . . . . 9 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → suc 𝑔 ⊆ dom 𝑇)
122	121	resabs1d 5975	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) = (𝑇 ↾ suc 𝑔))
123	121	resabs1d 5975	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔) = (𝑍 ↾ suc 𝑔))
124	122, 123	breq12d 5113	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → (((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔) ↔ (𝑇 ↾ suc 𝑔) <s (𝑍 ↾ suc 𝑔)))
125	117, 124	mtbird 325	. . . . . 6 ⊢ (((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) ∧ 𝑔 ∈ dom 𝑇) → ¬ ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔))
126	125	ralrimiva 3130	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ∀𝑔 ∈ dom 𝑇 ¬ ((𝑇 ↾ dom 𝑇) ↾ suc 𝑔) <s ((𝑍 ↾ dom 𝑇) ↾ suc 𝑔))
127		noresle 27677	. . . . 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 1380	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ¬ (𝑇 ↾ dom 𝑇) <s (𝑍 ↾ dom 𝑇))
129	69	breq1d 5110	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ((𝑇 ↾ dom 𝑇) <s (𝑍 ↾ dom 𝑇) ↔ 𝑇 <s (𝑍 ↾ dom 𝑇)))
130	128, 129	mtbid 324	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
131	55, 130	pm2.61ian 812	. 2 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
132		simplr 769	. . . . 5 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → ¬ 𝑇 <s (𝑍 ↾ dom 𝑇))
133		simpll1 1214	. . . . . 6 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝐵 ⊆ No )
134		simpll2 1215	. . . . . 6 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝐵 ∈ 𝑉)
135		simpr 484	. . . . . 6 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵)
136	2	noinfbnd1 27709	. . . . . 6 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑏 ∈ 𝐵) → 𝑇 <s (𝑏 ↾ dom 𝑇))
137	133, 134, 135, 136	syl3anc 1374	. . . . 5 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝑇 <s (𝑏 ↾ dom 𝑇))
138		simpl3 1195	. . . . . . . 8 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝑍 ∈ No )
139		simpl1 1193	. . . . . . . . . 10 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝐵 ⊆ No )
140		simpl2 1194	. . . . . . . . . 10 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝐵 ∈ 𝑉)
141	139, 140, 57	syl2anc 585	. . . . . . . . 9 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → 𝑇 ∈ No )
142	141, 60	syl 17	. . . . . . . 8 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → dom 𝑇 ∈ On)
143	138, 142, 62	syl2anc 585	. . . . . . 7 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) ∈ No )
144	143	adantr 480	. . . . . 6 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → (𝑍 ↾ dom 𝑇) ∈ No )
145	141	adantr 480	. . . . . 6 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝑇 ∈ No )
146	139	sselda 3935	. . . . . . 7 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No )
147	142	adantr 480	. . . . . . 7 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → dom 𝑇 ∈ On)
148		noreson 27640	. . . . . . 7 ⊢ ((𝑏 ∈ No ∧ dom 𝑇 ∈ On) → (𝑏 ↾ dom 𝑇) ∈ No )
149	146, 147, 148	syl2anc 585	. . . . . 6 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → (𝑏 ↾ dom 𝑇) ∈ No )
150		sotr2 5574	. . . . . . 7 ⊢ (( <s Or No ∧ ((𝑍 ↾ dom 𝑇) ∈ No ∧ 𝑇 ∈ No ∧ (𝑏 ↾ dom 𝑇) ∈ No )) → ((¬ 𝑇 <s (𝑍 ↾ dom 𝑇) ∧ 𝑇 <s (𝑏 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇)))
151	100, 150	mpan 691	. . . . . 6 ⊢ (((𝑍 ↾ dom 𝑇) ∈ No ∧ 𝑇 ∈ No ∧ (𝑏 ↾ dom 𝑇) ∈ No ) → ((¬ 𝑇 <s (𝑍 ↾ dom 𝑇) ∧ 𝑇 <s (𝑏 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇)))
152	144, 145, 149, 151	syl3anc 1374	. . . . 5 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → ((¬ 𝑇 <s (𝑍 ↾ dom 𝑇) ∧ 𝑇 <s (𝑏 ↾ dom 𝑇)) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇)))
153	132, 137, 152	mp2and 700	. . . 4 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → (𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇))
154		simpll3 1216	. . . . 5 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝑍 ∈ No )
155		ltsres 27642	. . . . 5 ⊢ ((𝑍 ∈ No ∧ 𝑏 ∈ No ∧ dom 𝑇 ∈ On) → ((𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇) → 𝑍 <s 𝑏))
156	154, 146, 147, 155	syl3anc 1374	. . . 4 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → ((𝑍 ↾ dom 𝑇) <s (𝑏 ↾ dom 𝑇) → 𝑍 <s 𝑏))
157	153, 156	mpd 15	. . 3 ⊢ ((((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) ∧ 𝑏 ∈ 𝐵) → 𝑍 <s 𝑏)
158	157	ralrimiva 3130	. 2 ⊢ (((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) ∧ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)) → ∀𝑏 ∈ 𝐵 𝑍 <s 𝑏)
159	131, 158	impbida 801	1 ⊢ ((𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ No ) → (∀𝑏 ∈ 𝐵 𝑍 <s 𝑏 ↔ ¬ 𝑇 <s (𝑍 ↾ dom 𝑇)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 {cab 2715 ∀wral 3052 ∃wrex 3062 ∃!wreu 3350 ∃*wrmo 3351 ∪ cun 3901 ⊆ wss 3903 ifcif 4481 {csn 4582 ⟨cop 4588 class class class wbr 5100 ↦ cmpt 5181 Or wor 5539 dom cdm 5632 ↾ cres 5634 Rel wrel 5637 Ord word 6324 Oncon0 6325 suc csuc 6327 ℩cio 6454 Fun wfun 6494 ‘cfv 6500 ℩crio 7324 1_oc1o 8400 No csur 27619 <s clts 27620

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-ord 6328 df-on 6329 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-1o 8407 df-2o 8408 df-no 27622 df-lts 27623 df-bday 27624

This theorem is referenced by: nosupinfsep 27712 noetainflem4 27720

W3C validator