Metamath Proof Explorer

Theorem nosupno

Description: The next several theorems deal with a surreal "supremum". This surreal will ultimately be shown to bound A below and bound the restriction of any surreal above. We begin by showing that the given expression actually defines a surreal number. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Hypothesis nosupno.1 $⊢ S = if ∃ x ∈ A ∀ y ∈ A ¬ x < s y ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
Assertion nosupno $⊢ A ⊆ No ∧ A ∈ V → S ∈ No$

Proof

Step Hyp Ref Expression
1 nosupno.1 $⊢ S = if ∃ x ∈ A ∀ y ∈ A ¬ x < s y ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
2 elex $⊢ A ∈ V → A ∈ V$
3 iftrue $⊢ ∃ x ∈ A ∀ y ∈ A ¬ x < s y → if ∃ x ∈ A ∀ y ∈ A ¬ x < s y ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x = ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜$
4 3 adantr $⊢ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → if ∃ x ∈ A ∀ y ∈ A ¬ x < s y ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x = ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜$
5 simprl $⊢ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → A ⊆ No$
6 simpl $⊢ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → ∃ x ∈ A ∀ y ∈ A ¬ x < s y$
7 nomaxmo $⊢ A ⊆ No → ∃* x ∈ A ∀ y ∈ A ¬ x < s y$
8 7 ad2antrl $⊢ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → ∃* x ∈ A ∀ y ∈ A ¬ x < s y$
9 reu5 $⊢ ∃! x ∈ A ∀ y ∈ A ¬ x < s y ↔ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ ∃* x ∈ A ∀ y ∈ A ¬ x < s y$
10 6 8 9 sylanbrc $⊢ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → ∃! x ∈ A ∀ y ∈ A ¬ x < s y$
11 riotacl $⊢ ∃! x ∈ A ∀ y ∈ A ¬ x < s y → ι x ∈ A | ∀ y ∈ A ¬ x < s y ∈ A$
12 10 11 syl $⊢ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → ι x ∈ A | ∀ y ∈ A ¬ x < s y ∈ A$
13 5 12 sseldd $⊢ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → ι x ∈ A | ∀ y ∈ A ¬ x < s y ∈ No$
14 2on $⊢ 2 𝑜 ∈ On$
15 14 elexi $⊢ 2 𝑜 ∈ V$
16 15 prid2 $⊢ 2 𝑜 ∈ 1 𝑜 2 𝑜$
17 16 noextend $⊢ ι x ∈ A | ∀ y ∈ A ¬ x < s y ∈ No → ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 ∈ No$
18 13 17 syl $⊢ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 ∈ No$
19 4 18 eqeltrd $⊢ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → if ∃ x ∈ A ∀ y ∈ A ¬ x < s y ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ∈ No$
20 iffalse $⊢ ¬ ∃ x ∈ A ∀ y ∈ A ¬ x < s y → if ∃ x ∈ A ∀ y ∈ A ¬ x < s y ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x = g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
21 20 adantr $⊢ ¬ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → if ∃ x ∈ A ∀ y ∈ A ¬ x < s y ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x = g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
22 funmpt $⊢ Fun ⁡ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
23 22 a1i $⊢ ¬ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → Fun ⁡ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
24 iotaex $⊢ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ∈ V$
25 eqid $⊢ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x = g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
26 24 25 dmmpti $⊢ dom ⁡ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x = y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y$
27 ssel2 $⊢ A ⊆ No ∧ u ∈ A → u ∈ No$
28 nodmon $⊢ u ∈ No → dom ⁡ u ∈ On$
29 27 28 syl $⊢ A ⊆ No ∧ u ∈ A → dom ⁡ u ∈ On$
30 onss $⊢ dom ⁡ u ∈ On → dom ⁡ u ⊆ On$
31 29 30 syl $⊢ A ⊆ No ∧ u ∈ A → dom ⁡ u ⊆ On$
32 31 sseld $⊢ A ⊆ No ∧ u ∈ A → y ∈ dom ⁡ u → y ∈ On$
33 32 adantrd $⊢ A ⊆ No ∧ u ∈ A → y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y → y ∈ On$
34 33 rexlimdva $⊢ A ⊆ No → ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y → y ∈ On$
35 34 abssdv $⊢ A ⊆ No → y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⊆ On$
36 simplr $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A → a ∈ b$
37 29 adantlr $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A → dom ⁡ u ∈ On$
38 ontr1 $⊢ dom ⁡ u ∈ On → a ∈ b ∧ b ∈ dom ⁡ u → a ∈ dom ⁡ u$
39 37 38 syl $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A → a ∈ b ∧ b ∈ dom ⁡ u → a ∈ dom ⁡ u$
40 36 39 mpand $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A → b ∈ dom ⁡ u → a ∈ dom ⁡ u$
41 40 adantrd $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A → b ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b → a ∈ dom ⁡ u$
42 reseq1 $⊢ u ↾ suc ⁡ b = v ↾ suc ⁡ b → u ↾ suc ⁡ b ↾ suc ⁡ a = v ↾ suc ⁡ b ↾ suc ⁡ a$
43 onelon $⊢ dom ⁡ u ∈ On ∧ b ∈ dom ⁡ u → b ∈ On$
44 37 43 sylan $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → b ∈ On$
45 suceloni $⊢ b ∈ On → suc ⁡ b ∈ On$
46 44 45 syl $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → suc ⁡ b ∈ On$
47 simpllr $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → a ∈ b$
48 eloni $⊢ b ∈ On → Ord ⁡ b$
49 44 48 syl $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → Ord ⁡ b$
50 ordsucelsuc $⊢ Ord ⁡ b → a ∈ b ↔ suc ⁡ a ∈ suc ⁡ b$
51 49 50 syl $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → a ∈ b ↔ suc ⁡ a ∈ suc ⁡ b$
52 47 51 mpbid $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → suc ⁡ a ∈ suc ⁡ b$
53 onelss $⊢ suc ⁡ b ∈ On → suc ⁡ a ∈ suc ⁡ b → suc ⁡ a ⊆ suc ⁡ b$
54 46 52 53 sylc $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → suc ⁡ a ⊆ suc ⁡ b$
55 54 resabs1d $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → u ↾ suc ⁡ b ↾ suc ⁡ a = u ↾ suc ⁡ a$
56 54 resabs1d $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → v ↾ suc ⁡ b ↾ suc ⁡ a = v ↾ suc ⁡ a$
57 55 56 eqeq12d $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → u ↾ suc ⁡ b ↾ suc ⁡ a = v ↾ suc ⁡ b ↾ suc ⁡ a ↔ u ↾ suc ⁡ a = v ↾ suc ⁡ a$
58 42 57 syl5ib $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → u ↾ suc ⁡ b = v ↾ suc ⁡ b → u ↾ suc ⁡ a = v ↾ suc ⁡ a$
59 58 imim2d $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b → ¬ v < s u → u ↾ suc ⁡ a = v ↾ suc ⁡ a$
60 59 ralimdv $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A ∧ b ∈ dom ⁡ u → ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b → ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ a = v ↾ suc ⁡ a$
61 60 expimpd $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A → b ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b → ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ a = v ↾ suc ⁡ a$
62 41 61 jcad $⊢ A ⊆ No ∧ a ∈ b ∧ u ∈ A → b ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b → a ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ a = v ↾ suc ⁡ a$
63 62 reximdva $⊢ A ⊆ No ∧ a ∈ b → ∃ u ∈ A b ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b → ∃ u ∈ A a ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ a = v ↾ suc ⁡ a$
64 63 expimpd $⊢ A ⊆ No → a ∈ b ∧ ∃ u ∈ A b ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b → ∃ u ∈ A a ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ a = v ↾ suc ⁡ a$
65 vex $⊢ b ∈ V$
66 eleq1w $⊢ y = b → y ∈ dom ⁡ u ↔ b ∈ dom ⁡ u$
67 suceq $⊢ y = b → suc ⁡ y = suc ⁡ b$
68 67 reseq2d $⊢ y = b → u ↾ suc ⁡ y = u ↾ suc ⁡ b$
69 67 reseq2d $⊢ y = b → v ↾ suc ⁡ y = v ↾ suc ⁡ b$
70 68 69 eqeq12d $⊢ y = b → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ u ↾ suc ⁡ b = v ↾ suc ⁡ b$
71 70 imbi2d $⊢ y = b → ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b$
72 71 ralbidv $⊢ y = b → ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b$
73 66 72 anbi12d $⊢ y = b → y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ b ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b$
74 73 rexbidv $⊢ y = b → ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ∃ u ∈ A b ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b$
75 65 74 elab $⊢ b ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ∃ u ∈ A b ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b$
76 75 anbi2i $⊢ a ∈ b ∧ b ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ a ∈ b ∧ ∃ u ∈ A b ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ b = v ↾ suc ⁡ b$
77 vex $⊢ a ∈ V$
78 eleq1w $⊢ y = a → y ∈ dom ⁡ u ↔ a ∈ dom ⁡ u$
79 suceq $⊢ y = a → suc ⁡ y = suc ⁡ a$
80 79 reseq2d $⊢ y = a → u ↾ suc ⁡ y = u ↾ suc ⁡ a$
81 79 reseq2d $⊢ y = a → v ↾ suc ⁡ y = v ↾ suc ⁡ a$
82 80 81 eqeq12d $⊢ y = a → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ u ↾ suc ⁡ a = v ↾ suc ⁡ a$
83 82 imbi2d $⊢ y = a → ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ¬ v < s u → u ↾ suc ⁡ a = v ↾ suc ⁡ a$
84 83 ralbidv $⊢ y = a → ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ a = v ↾ suc ⁡ a$
85 78 84 anbi12d $⊢ y = a → y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ a ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ a = v ↾ suc ⁡ a$
86 85 rexbidv $⊢ y = a → ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ∃ u ∈ A a ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ a = v ↾ suc ⁡ a$
87 77 86 elab $⊢ a ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ∃ u ∈ A a ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ a = v ↾ suc ⁡ a$
88 64 76 87 3imtr4g $⊢ A ⊆ No → a ∈ b ∧ b ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y → a ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y$
89 88 alrimivv $⊢ A ⊆ No → ∀ a ∀ b a ∈ b ∧ b ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y → a ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y$
90 dftr2 $⊢ Tr ⁡ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ∀ a ∀ b a ∈ b ∧ b ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y → a ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y$
91 89 90 sylibr $⊢ A ⊆ No → Tr ⁡ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y$
92 dford5 $⊢ Ord ⁡ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⊆ On ∧ Tr ⁡ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y$
93 35 91 92 sylanbrc $⊢ A ⊆ No → Ord ⁡ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y$
94 93 adantr $⊢ A ⊆ No ∧ A ∈ V → Ord ⁡ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y$
95 bdayfo $⊢ bday : No ⟶ onto On$
96 fofun $⊢ bday : No ⟶ onto On → Fun ⁡ bday$
97 95 96 ax-mp $⊢ Fun ⁡ bday$
98 funimaexg $⊢ Fun ⁡ bday ∧ A ∈ V → bday A ∈ V$
99 97 98 mpan $⊢ A ∈ V → bday A ∈ V$
100 99 uniexd $⊢ A ∈ V → ⋃ bday A ∈ V$
101 100 adantl $⊢ A ⊆ No ∧ A ∈ V → ⋃ bday A ∈ V$
102 simpl $⊢ y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y → y ∈ dom ⁡ u$
103 102 reximi $⊢ ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y → ∃ u ∈ A y ∈ dom ⁡ u$
104 103 ss2abi $⊢ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⊆ y | ∃ u ∈ A y ∈ dom ⁡ u$
105 bdayval $⊢ u ∈ No → bday ⁡ u = dom ⁡ u$
106 27 105 syl $⊢ A ⊆ No ∧ u ∈ A → bday ⁡ u = dom ⁡ u$
107 fofn $⊢ bday : No ⟶ onto On → bday Fn No$
108 95 107 ax-mp $⊢ bday Fn No$
109 fnfvima $⊢ bday Fn No ∧ A ⊆ No ∧ u ∈ A → bday ⁡ u ∈ bday A$
110 108 109 mp3an1 $⊢ A ⊆ No ∧ u ∈ A → bday ⁡ u ∈ bday A$
111 106 110 eqeltrrd $⊢ A ⊆ No ∧ u ∈ A → dom ⁡ u ∈ bday A$
112 elssuni $⊢ dom ⁡ u ∈ bday A → dom ⁡ u ⊆ ⋃ bday A$
113 111 112 syl $⊢ A ⊆ No ∧ u ∈ A → dom ⁡ u ⊆ ⋃ bday A$
114 113 sseld $⊢ A ⊆ No ∧ u ∈ A → y ∈ dom ⁡ u → y ∈ ⋃ bday A$
115 114 rexlimdva $⊢ A ⊆ No → ∃ u ∈ A y ∈ dom ⁡ u → y ∈ ⋃ bday A$
116 115 abssdv $⊢ A ⊆ No → y | ∃ u ∈ A y ∈ dom ⁡ u ⊆ ⋃ bday A$
117 116 adantr $⊢ A ⊆ No ∧ A ∈ V → y | ∃ u ∈ A y ∈ dom ⁡ u ⊆ ⋃ bday A$
118 104 117 sstrid $⊢ A ⊆ No ∧ A ∈ V → y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⊆ ⋃ bday A$
119 101 118 ssexd $⊢ A ⊆ No ∧ A ∈ V → y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ∈ V$
120 elong $⊢ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ∈ V → y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ∈ On ↔ Ord ⁡ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y$
121 119 120 syl $⊢ A ⊆ No ∧ A ∈ V → y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ∈ On ↔ Ord ⁡ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y$
122 94 121 mpbird $⊢ A ⊆ No ∧ A ∈ V → y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ∈ On$
123 26 122 eqeltrid $⊢ A ⊆ No ∧ A ∈ V → dom ⁡ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ∈ On$
124 123 adantl $⊢ ¬ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → dom ⁡ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ∈ On$
125 25 rnmpt $⊢ ran ⁡ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x = z | ∃ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y z = ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
126 vex $⊢ g ∈ V$
127 eleq1w $⊢ y = g → y ∈ dom ⁡ u ↔ g ∈ dom ⁡ u$
128 suceq $⊢ y = g → suc ⁡ y = suc ⁡ g$
129 128 reseq2d $⊢ y = g → u ↾ suc ⁡ y = u ↾ suc ⁡ g$
130 128 reseq2d $⊢ y = g → v ↾ suc ⁡ y = v ↾ suc ⁡ g$
131 129 130 eqeq12d $⊢ y = g → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ u ↾ suc ⁡ g = v ↾ suc ⁡ g$
132 131 imbi2d $⊢ y = g → ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g$
133 132 ralbidv $⊢ y = g → ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g$
134 127 133 anbi12d $⊢ y = g → y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g$
135 134 rexbidv $⊢ y = g → ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g$
136 126 135 elab $⊢ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ↔ ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g$
137 eqid $⊢ u ⁡ g = u ⁡ g$
138 fvex $⊢ u ⁡ g ∈ V$
139 eqeq2 $⊢ x = u ⁡ g → u ⁡ g = x ↔ u ⁡ g = u ⁡ g$
140 139 3anbi3d $⊢ x = u ⁡ g → g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ↔ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = u ⁡ g$
141 138 140 spcev $⊢ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = u ⁡ g → ∃ x g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
142 137 141 mp3an3 $⊢ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g → ∃ x g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
143 142 reximi $⊢ ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g → ∃ u ∈ A ∃ x g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
144 rexcom4 $⊢ ∃ u ∈ A ∃ x g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ↔ ∃ x ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
145 143 144 sylib $⊢ ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g → ∃ x ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
146 145 adantl $⊢ A ⊆ No ∧ ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g → ∃ x ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
147 nosupprefixmo $⊢ A ⊆ No → ∃* x ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
148 147 adantr $⊢ A ⊆ No ∧ ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g → ∃* x ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
149 df-eu $⊢ ∃! x ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ↔ ∃ x ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ∧ ∃* x ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
150 146 148 149 sylanbrc $⊢ A ⊆ No ∧ ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g → ∃! x ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
151 vex $⊢ z ∈ V$
152 eqeq2 $⊢ x = z → u ⁡ g = x ↔ u ⁡ g = z$
153 152 3anbi3d $⊢ x = z → g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ↔ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z$
154 153 rexbidv $⊢ x = z → ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ↔ ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z$
155 154 iota2 $⊢ z ∈ V ∧ ∃! x ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x → ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z ↔ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x = z$
156 151 155 mpan $⊢ ∃! x ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x → ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z ↔ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x = z$
157 150 156 syl $⊢ A ⊆ No ∧ ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g → ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z ↔ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x = z$
158 eqcom $⊢ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x = z ↔ z = ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
159 157 158 syl6bb $⊢ A ⊆ No ∧ ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g → ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z ↔ z = ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x$
160 simprr3 $⊢ A ⊆ No ∧ u ∈ A ∧ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z → u ⁡ g = z$
161 27 adantrr $⊢ A ⊆ No ∧ u ∈ A ∧ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z → u ∈ No$
162 norn $⊢ u ∈ No → ran ⁡ u ⊆ 1 𝑜 2 𝑜$
163 161 162 syl $⊢ A ⊆ No ∧ u ∈ A ∧ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z → ran ⁡ u ⊆ 1 𝑜 2 𝑜$
164 nofun $⊢ u ∈ No → Fun ⁡ u$
165 161 164 syl $⊢ A ⊆ No ∧ u ∈ A ∧ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z → Fun ⁡ u$
166 simprr1 $⊢ A ⊆ No ∧ u ∈ A ∧ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z → g ∈ dom ⁡ u$
167 fvelrn $⊢ Fun ⁡ u ∧ g ∈ dom ⁡ u → u ⁡ g ∈ ran ⁡ u$
168 165 166 167 syl2anc $⊢ A ⊆ No ∧ u ∈ A ∧ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z → u ⁡ g ∈ ran ⁡ u$
169 163 168 sseldd $⊢ A ⊆ No ∧ u ∈ A ∧ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z → u ⁡ g ∈ 1 𝑜 2 𝑜$
170 160 169 eqeltrrd $⊢ A ⊆ No ∧ u ∈ A ∧ g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z → z ∈ 1 𝑜 2 𝑜$
171 170 rexlimdvaa $⊢ A ⊆ No → ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z → z ∈ 1 𝑜 2 𝑜$
172 171 adantr $⊢ A ⊆ No ∧ ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g → ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = z → z ∈ 1 𝑜 2 𝑜$
173 159 172 sylbird $⊢ A ⊆ No ∧ ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g → z = ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x → z ∈ 1 𝑜 2 𝑜$
174 136 173 sylan2b $⊢ A ⊆ No ∧ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y → z = ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x → z ∈ 1 𝑜 2 𝑜$
175 174 rexlimdva $⊢ A ⊆ No → ∃ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y z = ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x → z ∈ 1 𝑜 2 𝑜$
176 175 abssdv $⊢ A ⊆ No → z | ∃ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y z = ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ⊆ 1 𝑜 2 𝑜$
177 125 176 eqsstrid $⊢ A ⊆ No → ran ⁡ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ⊆ 1 𝑜 2 𝑜$
178 177 ad2antrl $⊢ ¬ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → ran ⁡ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ⊆ 1 𝑜 2 𝑜$
179 elno2 $⊢ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ∈ No ↔ Fun ⁡ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ∧ dom ⁡ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ∈ On ∧ ran ⁡ g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ⊆ 1 𝑜 2 𝑜$
180 23 124 178 179 syl3anbrc $⊢ ¬ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ∈ No$
181 21 180 eqeltrd $⊢ ¬ ∃ x ∈ A ∀ y ∈ A ¬ x < s y ∧ A ⊆ No ∧ A ∈ V → if ∃ x ∈ A ∀ y ∈ A ¬ x < s y ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ∈ No$
182 19 181 pm2.61ian $⊢ A ⊆ No ∧ A ∈ V → if ∃ x ∈ A ∀ y ∈ A ¬ x < s y ι x ∈ A | ∀ y ∈ A ¬ x < s y ∪ dom ⁡ ι x ∈ A | ∀ y ∈ A ¬ x < s y 2 𝑜 g ∈ y | ∃ u ∈ A y ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ A g ∈ dom ⁡ u ∧ ∀ v ∈ A ¬ v < s u → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x ∈ No$
183 1 182 eqeltrid $⊢ A ⊆ No ∧ A ∈ V → S ∈ No$
184 2 183 sylan2 $⊢ A ⊆ No ∧ A ∈ V → S ∈ No$