Metamath Proof Explorer

Theorem noinfno

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

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

Proof

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