nosupres - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > nosupres		Structured version Visualization version GIF version

Theorem nosupres 31853

Description: A restriction law for surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021.)

**Hypothesis**
Ref	Expression
nosupres.1	⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))

**Assertion**
Ref	Expression
nosupres	⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑆 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))

Distinct variable groups: 𝐴,𝑔,𝑢,𝑣,𝑥,𝑦 𝑢,𝐺 𝑣,𝑔 𝑣,𝐺 𝑥,𝑔,𝑦 𝑦,𝐺 𝑢,𝑈,𝑣,𝑥 𝑦,𝑢 𝑥,𝑣,𝑦 Allowed substitution hints: 𝑆(𝑥,𝑦,𝑣,𝑢,𝑔) 𝑈(𝑦,𝑔) 𝐺(𝑥,𝑔)

Proof of Theorem nosupres Dummy variables 𝑎 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmres 5419	. . . 4 ⊢ dom (𝑆 ↾ suc 𝐺) = (suc 𝐺 ∩ dom 𝑆)
2		nosupres.1	. . . . . . . . 9 ⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
3	2	nosupno 31849	. . . . . . . 8 ⊢ ((𝐴 ⊆ No ∧ 𝐴 ∈ V) → 𝑆 ∈ No )
4	3	3ad2ant2 1083	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝑆 ∈ No )
5		nodmord 31806	. . . . . . 7 ⊢ (𝑆 ∈ No → Ord dom 𝑆)
6	4, 5	syl 17	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Ord dom 𝑆)
7		dmeq 5324	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑈 → dom 𝑝 = dom 𝑈)
8	7	eleq2d 2687	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑈 → (𝐺 ∈ dom 𝑝 ↔ 𝐺 ∈ dom 𝑈))
9		breq2 4657	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑈 → (𝑣 <s 𝑝 ↔ 𝑣 <s 𝑈))
10	9	notbid 308	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑈 → (¬ 𝑣 <s 𝑝 ↔ ¬ 𝑣 <s 𝑈))
11		reseq1 5390	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑈 → (𝑝 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))
12	11	eqeq1d 2624	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑈 → ((𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
13	10, 12	imbi12d 334	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑈 → ((¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
14	13	ralbidv 2986	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑈 → (∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
15	8, 14	anbi12d 747	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑈 → ((𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) ↔ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
16	15	rspcev 3309	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ 𝐴 ∧ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
17	16	3impb 1260	. . . . . . . . . 10 ⊢ ((𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
18		dmeq 5324	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
19	18	eleq2d 2687	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑝 → (𝐺 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑝))
20		breq2 4657	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑝 → (𝑣 <s 𝑢 ↔ 𝑣 <s 𝑝))
21	20	notbid 308	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑝 → (¬ 𝑣 <s 𝑢 ↔ ¬ 𝑣 <s 𝑝))
22		reseq1 5390	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
23	22	eqeq1d 2624	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
24	21, 23	imbi12d 334	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑝 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
25	24	ralbidv 2986	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑝 → (∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
26	19, 25	anbi12d 747	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑝 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) ↔ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
27	26	cbvrexv 3172	. . . . . . . . . 10 ⊢ (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) ↔ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
28	17, 27	sylibr 224	. . . . . . . . 9 ⊢ ((𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
29		eleq1 2689	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐺 → (𝑦 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑢))
30		suceq 5790	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝐺 → suc 𝑦 = suc 𝐺)
31	30	reseq2d 5396	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐺 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝐺))
32	30	reseq2d 5396	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝐺 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝐺))
33	31, 32	eqeq12d 2637	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝐺 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
34	33	imbi2d 330	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝐺 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
35	34	ralbidv 2986	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝐺 → (∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
36	29, 35	anbi12d 747	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝐺 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
37	36	rexbidv 3052	. . . . . . . . . . 11 ⊢ (𝑦 = 𝐺 → (∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
38	37	elabg 3351	. . . . . . . . . 10 ⊢ (𝐺 ∈ dom 𝑈 → (𝐺 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
39	38	3ad2ant2 1083	. . . . . . . . 9 ⊢ ((𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → (𝐺 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
40	28, 39	mpbird 247	. . . . . . . 8 ⊢ ((𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → 𝐺 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
41	40	3ad2ant3 1084	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
42		iffalse 4095	. . . . . . . . . . 11 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2_𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
43	2, 42	syl5eq 2668	. . . . . . . . . 10 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
44	43	dmeqd 5326	. . . . . . . . 9 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))))
45		iotaex 5868	. . . . . . . . . 10 ⊢ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) ∈ V
46		eqid 2622	. . . . . . . . . 10 ⊢ (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))
47	45, 46	dmmpti 6023	. . . . . . . . 9 ⊢ dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
48	44, 47	syl6eq 2672	. . . . . . . 8 ⊢ (¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
49	48	3ad2ant1 1082	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom 𝑆 = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
50	41, 49	eleqtrrd 2704	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ dom 𝑆)
51		ordsucss 7018	. . . . . 6 ⊢ (Ord dom 𝑆 → (𝐺 ∈ dom 𝑆 → suc 𝐺 ⊆ dom 𝑆))
52	6, 50, 51	sylc 65	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → suc 𝐺 ⊆ dom 𝑆)
53		df-ss 3588	. . . . 5 ⊢ (suc 𝐺 ⊆ dom 𝑆 ↔ (suc 𝐺 ∩ dom 𝑆) = suc 𝐺)
54	52, 53	sylib 208	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (suc 𝐺 ∩ dom 𝑆) = suc 𝐺)
55	1, 54	syl5eq 2668	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom (𝑆 ↾ suc 𝐺) = suc 𝐺)
56		dmres 5419	. . . 4 ⊢ dom (𝑈 ↾ suc 𝐺) = (suc 𝐺 ∩ dom 𝑈)
57		simp2l 1087	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐴 ⊆ No )
58		simp31 1097	. . . . . . . 8 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝑈 ∈ 𝐴)
59	57, 58	sseldd 3604	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝑈 ∈ No )
60		nodmord 31806	. . . . . . 7 ⊢ (𝑈 ∈ No → Ord dom 𝑈)
61	59, 60	syl 17	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Ord dom 𝑈)
62		simp32 1098	. . . . . 6 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ dom 𝑈)
63		ordsucss 7018	. . . . . 6 ⊢ (Ord dom 𝑈 → (𝐺 ∈ dom 𝑈 → suc 𝐺 ⊆ dom 𝑈))
64	61, 62, 63	sylc 65	. . . . 5 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → suc 𝐺 ⊆ dom 𝑈)
65		df-ss 3588	. . . . 5 ⊢ (suc 𝐺 ⊆ dom 𝑈 ↔ (suc 𝐺 ∩ dom 𝑈) = suc 𝐺)
66	64, 65	sylib 208	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (suc 𝐺 ∩ dom 𝑈) = suc 𝐺)
67	56, 66	syl5eq 2668	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom (𝑈 ↾ suc 𝐺) = suc 𝐺)
68	55, 67	eqtr4d 2659	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom (𝑆 ↾ suc 𝐺) = dom (𝑈 ↾ suc 𝐺))
69	55	eleq2d 2687	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ dom (𝑆 ↾ suc 𝐺) ↔ 𝑎 ∈ suc 𝐺))
70		simpl1 1064	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)
71		simpl2 1065	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → (𝐴 ⊆ No ∧ 𝐴 ∈ V))
72		simpl31 1142	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑈 ∈ 𝐴)
73	64	sselda 3603	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑎 ∈ dom 𝑈)
74		nodmon 31803	. . . . . . . . . . . . . 14 ⊢ (𝑈 ∈ No → dom 𝑈 ∈ On)
75	59, 74	syl 17	. . . . . . . . . . . . 13 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom 𝑈 ∈ On)
76		onelon 5748	. . . . . . . . . . . . 13 ⊢ ((dom 𝑈 ∈ On ∧ 𝐺 ∈ dom 𝑈) → 𝐺 ∈ On)
77	75, 62, 76	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ On)
78		eloni 5733	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ On → Ord 𝐺)
79	77, 78	syl 17	. . . . . . . . . . 11 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Ord 𝐺)
80		ordsuc 7014	. . . . . . . . . . 11 ⊢ (Ord 𝐺 ↔ Ord suc 𝐺)
81	79, 80	sylib 208	. . . . . . . . . 10 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Ord suc 𝐺)
82		ordsucss 7018	. . . . . . . . . 10 ⊢ (Ord suc 𝐺 → (𝑎 ∈ suc 𝐺 → suc 𝑎 ⊆ suc 𝐺))
83	81, 82	syl 17	. . . . . . . . 9 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ suc 𝐺 → suc 𝑎 ⊆ suc 𝐺))
84	83	imp 445	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → suc 𝑎 ⊆ suc 𝐺)
85		simpl33 1144	. . . . . . . 8 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
86		reseq1 5390	. . . . . . . . . . 11 ⊢ ((𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) → ((𝑈 ↾ suc 𝐺) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝐺) ↾ suc 𝑎))
87		resabs1 5427	. . . . . . . . . . . 12 ⊢ (suc 𝑎 ⊆ suc 𝐺 → ((𝑈 ↾ suc 𝐺) ↾ suc 𝑎) = (𝑈 ↾ suc 𝑎))
88		resabs1 5427	. . . . . . . . . . . 12 ⊢ (suc 𝑎 ⊆ suc 𝐺 → ((𝑣 ↾ suc 𝐺) ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))
89	87, 88	eqeq12d 2637	. . . . . . . . . . 11 ⊢ (suc 𝑎 ⊆ suc 𝐺 → (((𝑈 ↾ suc 𝐺) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝐺) ↾ suc 𝑎) ↔ (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
90	86, 89	syl5ib 234	. . . . . . . . . 10 ⊢ (suc 𝑎 ⊆ suc 𝐺 → ((𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
91	90	imim2d 57	. . . . . . . . 9 ⊢ (suc 𝑎 ⊆ suc 𝐺 → ((¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) → (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
92	91	ralimdv 2963	. . . . . . . 8 ⊢ (suc 𝑎 ⊆ suc 𝐺 → (∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) → ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
93	84, 85, 92	sylc 65	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
94	2	nosupfv 31852	. . . . . . 7 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝑎 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))) → (𝑆‘𝑎) = (𝑈‘𝑎))
95	70, 71, 72, 73, 93, 94	syl113anc 1338	. . . . . 6 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → (𝑆‘𝑎) = (𝑈‘𝑎))
96		simpr 477	. . . . . . 7 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑎 ∈ suc 𝐺)
97	96	fvresd 6208	. . . . . 6 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ((𝑆 ↾ suc 𝐺)‘𝑎) = (𝑆‘𝑎))
98	96	fvresd 6208	. . . . . 6 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ((𝑈 ↾ suc 𝐺)‘𝑎) = (𝑈‘𝑎))
99	95, 97, 98	3eqtr4d 2666	. . . . 5 ⊢ (((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ((𝑆 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))
100	99	ex 450	. . . 4 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ suc 𝐺 → ((𝑆 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎)))
101	69, 100	sylbid 230	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ dom (𝑆 ↾ suc 𝐺) → ((𝑆 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎)))
102	101	ralrimiv 2965	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∀𝑎 ∈ dom (𝑆 ↾ suc 𝐺)((𝑆 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))
103		nofun 31802	. . . 4 ⊢ (𝑆 ∈ No → Fun 𝑆)
104		funres 5929	. . . 4 ⊢ (Fun 𝑆 → Fun (𝑆 ↾ suc 𝐺))
105	4, 103, 104	3syl 18	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Fun (𝑆 ↾ suc 𝐺))
106		nofun 31802	. . . 4 ⊢ (𝑈 ∈ No → Fun 𝑈)
107		funres 5929	. . . 4 ⊢ (Fun 𝑈 → Fun (𝑈 ↾ suc 𝐺))
108	59, 106, 107	3syl 18	. . 3 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Fun (𝑈 ↾ suc 𝐺))
109		eqfunfv 6316	. . 3 ⊢ ((Fun (𝑆 ↾ suc 𝐺) ∧ Fun (𝑈 ↾ suc 𝐺)) → ((𝑆 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺) ↔ (dom (𝑆 ↾ suc 𝐺) = dom (𝑈 ↾ suc 𝐺) ∧ ∀𝑎 ∈ dom (𝑆 ↾ suc 𝐺)((𝑆 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))))
110	105, 108, 109	syl2anc 693	. 2 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ((𝑆 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺) ↔ (dom (𝑆 ↾ suc 𝐺) = dom (𝑈 ↾ suc 𝐺) ∧ ∀𝑎 ∈ dom (𝑆 ↾ suc 𝐺)((𝑆 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))))
111	68, 102, 110	mpbir2and 957	1 ⊢ ((¬ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝑈 ∈ 𝐴 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑆 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 {cab 2608 ∀wral 2912 ∃wrex 2913 Vcvv 3200 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ifcif 4086 {csn 4177 ⟨cop 4183 class class class wbr 4653 ↦ cmpt 4729 dom cdm 5114 ↾ cres 5116 Ord word 5722 Oncon0 5723 suc csuc 5725 ℩cio 5849 Fun wfun 5882 ‘cfv 5888 ℩crio 6610 2_𝑜c2o 7554 No csur 31793 <s cslt 31794

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-ord 5726 df-on 5727 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-1o 7560 df-2o 7561 df-no 31796 df-slt 31797 df-bday 31798

This theorem is referenced by: nosupbnd1lem1 31854 nosupbnd2 31862

W3C validator