Metamath Proof Explorer

Theorem noinfres

Description: The restriction of surreal infimum when there is no minimum. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Hypothesis noinfres.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 noinfres ⊢ ¬ ∃ 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 → T ↾ suc ⁡ G = U ↾ suc ⁡ G

Proof

Step Hyp Ref Expression
1 noinfres.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 dmres ⊢ dom ⁡ T ↾ suc ⁡ G = suc ⁡ G ∩ dom ⁡ T
3 1 noinfno ⊢ B ⊆ No ∧ B ∈ V → T ∈ No
4 3 3ad2ant2 ⊢ ¬ ∃ 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 → T ∈ No
5 nodmord ⊢ T ∈ No → Ord ⁡ dom ⁡ T
6 4 5 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 → Ord ⁡ dom ⁡ T
7 simp31 ⊢ ¬ ∃ 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
8 simp32 ⊢ ¬ ∃ 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 → G ∈ dom ⁡ U
9 simp33 ⊢ ¬ ∃ 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 → ∀ v ∈ B ¬ U < s v → U ↾ suc ⁡ G = v ↾ suc ⁡ G
10 dmeq ⊢ b = U → dom ⁡ b = dom ⁡ U
11 10 eleq2d ⊢ b = U → G ∈ dom ⁡ b ↔ G ∈ dom ⁡ U
12 breq1 ⊢ b = U → b < s c ↔ U < s c
13 12 notbid ⊢ b = U → ¬ b < s c ↔ ¬ U < s c
14 reseq1 ⊢ b = U → b ↾ suc ⁡ G = U ↾ suc ⁡ G
15 14 eqeq1d ⊢ b = U → b ↾ suc ⁡ G = c ↾ suc ⁡ G ↔ U ↾ suc ⁡ G = c ↾ suc ⁡ G
16 13 15 imbi12d ⊢ b = U → ¬ b < s c → b ↾ suc ⁡ G = c ↾ suc ⁡ G ↔ ¬ U < s c → U ↾ suc ⁡ G = c ↾ suc ⁡ G
17 16 ralbidv ⊢ b = U → ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ G = c ↾ suc ⁡ G ↔ ∀ c ∈ B ¬ U < s c → U ↾ suc ⁡ G = c ↾ suc ⁡ G
18 breq2 ⊢ c = v → U < s c ↔ U < s v
19 18 notbid ⊢ c = v → ¬ U < s c ↔ ¬ U < s v
20 reseq1 ⊢ c = v → c ↾ suc ⁡ G = v ↾ suc ⁡ G
21 20 eqeq2d ⊢ c = v → U ↾ suc ⁡ G = c ↾ suc ⁡ G ↔ U ↾ suc ⁡ G = v ↾ suc ⁡ G
22 19 21 imbi12d ⊢ c = v → ¬ U < s c → U ↾ suc ⁡ G = c ↾ suc ⁡ G ↔ ¬ U < s v → U ↾ suc ⁡ G = v ↾ suc ⁡ G
23 22 cbvralvw ⊢ ∀ c ∈ B ¬ U < s c → U ↾ suc ⁡ G = c ↾ suc ⁡ G ↔ ∀ v ∈ B ¬ U < s v → U ↾ suc ⁡ G = v ↾ suc ⁡ G
24 17 23 bitrdi ⊢ b = U → ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ G = c ↾ suc ⁡ G ↔ ∀ v ∈ B ¬ U < s v → U ↾ suc ⁡ G = v ↾ suc ⁡ G
25 11 24 anbi12d ⊢ b = U → G ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ G = c ↾ suc ⁡ G ↔ G ∈ dom ⁡ U ∧ ∀ v ∈ B ¬ U < s v → U ↾ suc ⁡ G = v ↾ suc ⁡ G
26 25 rspcev ⊢ U ∈ B ∧ G ∈ dom ⁡ U ∧ ∀ v ∈ B ¬ U < s v → U ↾ suc ⁡ G = v ↾ suc ⁡ G → ∃ b ∈ B G ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ G = c ↾ suc ⁡ G
27 7 8 9 26 syl12anc ⊢ ¬ ∃ 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 → ∃ b ∈ B G ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ G = c ↾ suc ⁡ G
28 eleq1 ⊢ a = G → a ∈ dom ⁡ b ↔ G ∈ dom ⁡ b
29 suceq ⊢ a = G → suc ⁡ a = suc ⁡ G
30 29 reseq2d ⊢ a = G → b ↾ suc ⁡ a = b ↾ suc ⁡ G
31 29 reseq2d ⊢ a = G → c ↾ suc ⁡ a = c ↾ suc ⁡ G
32 30 31 eqeq12d ⊢ a = G → b ↾ suc ⁡ a = c ↾ suc ⁡ a ↔ b ↾ suc ⁡ G = c ↾ suc ⁡ G
33 32 imbi2d ⊢ a = G → ¬ b < s c → b ↾ suc ⁡ a = c ↾ suc ⁡ a ↔ ¬ b < s c → b ↾ suc ⁡ G = c ↾ suc ⁡ G
34 33 ralbidv ⊢ a = G → ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ a = c ↾ suc ⁡ a ↔ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ G = c ↾ suc ⁡ G
35 28 34 anbi12d ⊢ a = G → a ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ a = c ↾ suc ⁡ a ↔ G ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ G = c ↾ suc ⁡ G
36 35 rexbidv ⊢ a = G → ∃ b ∈ B a ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ a = c ↾ suc ⁡ a ↔ ∃ b ∈ B G ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ G = c ↾ suc ⁡ G
37 36 elabg ⊢ G ∈ dom ⁡ U → G ∈ a | ∃ b ∈ B a ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ a = c ↾ suc ⁡ a ↔ ∃ b ∈ B G ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ G = c ↾ suc ⁡ G
38 8 37 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 → G ∈ a | ∃ b ∈ B a ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ a = c ↾ suc ⁡ a ↔ ∃ b ∈ B G ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ G = c ↾ suc ⁡ G
39 27 38 mpbird ⊢ ¬ ∃ 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 → G ∈ a | ∃ b ∈ B a ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ a = c ↾ suc ⁡ a
40 1 noinfdm ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x → dom ⁡ T = a | ∃ b ∈ B a ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ a = c ↾ suc ⁡ a
41 40 3ad2ant1 ⊢ ¬ ∃ 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 → dom ⁡ T = a | ∃ b ∈ B a ∈ dom ⁡ b ∧ ∀ c ∈ B ¬ b < s c → b ↾ suc ⁡ a = c ↾ suc ⁡ a
42 39 41 eleqtrrd ⊢ ¬ ∃ 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 → G ∈ dom ⁡ T
43 ordsucss ⊢ Ord ⁡ dom ⁡ T → G ∈ dom ⁡ T → suc ⁡ G ⊆ dom ⁡ T
44 6 42 43 sylc ⊢ ¬ ∃ 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 → suc ⁡ G ⊆ dom ⁡ T
45 df-ss ⊢ suc ⁡ G ⊆ dom ⁡ T ↔ suc ⁡ G ∩ dom ⁡ T = suc ⁡ G
46 44 45 sylib ⊢ ¬ ∃ 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 → suc ⁡ G ∩ dom ⁡ T = suc ⁡ G
47 2 46 syl5eq ⊢ ¬ ∃ 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 → dom ⁡ T ↾ suc ⁡ G = suc ⁡ G
48 dmres ⊢ dom ⁡ U ↾ suc ⁡ G = suc ⁡ G ∩ dom ⁡ U
49 simp2l ⊢ ¬ ∃ 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 → B ⊆ No
50 49 7 sseldd ⊢ ¬ ∃ 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 ∈ No
51 nodmon ⊢ U ∈ No → dom ⁡ U ∈ On
52 50 51 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 → dom ⁡ U ∈ On
53 eloni ⊢ dom ⁡ U ∈ On → Ord ⁡ dom ⁡ U
54 52 53 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 → Ord ⁡ dom ⁡ U
55 ordsucss ⊢ Ord ⁡ dom ⁡ U → G ∈ dom ⁡ U → suc ⁡ G ⊆ dom ⁡ U
56 54 8 55 sylc ⊢ ¬ ∃ 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 → suc ⁡ G ⊆ dom ⁡ U
57 df-ss ⊢ suc ⁡ G ⊆ dom ⁡ U ↔ suc ⁡ G ∩ dom ⁡ U = suc ⁡ G
58 56 57 sylib ⊢ ¬ ∃ 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 → suc ⁡ G ∩ dom ⁡ U = suc ⁡ G
59 48 58 syl5eq ⊢ ¬ ∃ 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 → dom ⁡ U ↾ suc ⁡ G = suc ⁡ G
60 47 59 eqtr4d ⊢ ¬ ∃ 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 → dom ⁡ T ↾ suc ⁡ G = dom ⁡ U ↾ suc ⁡ G
61 47 eleq2d ⊢ ¬ ∃ 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 → a ∈ dom ⁡ T ↾ suc ⁡ G ↔ a ∈ suc ⁡ G
62 simpl1 ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x
63 simpl2 ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → B ⊆ No ∧ B ∈ V
64 simpl31 ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → U ∈ B
65 56 sselda ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → a ∈ dom ⁡ U
66 50 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 ∧ a ∈ suc ⁡ G → U ∈ No
67 66 51 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 ∧ a ∈ suc ⁡ G → dom ⁡ U ∈ On
68 simpl32 ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → G ∈ dom ⁡ U
69 onelon ⊢ dom ⁡ U ∈ On ∧ G ∈ dom ⁡ U → G ∈ On
70 67 68 69 syl2anc ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → G ∈ On
71 sucelon ⊢ G ∈ On ↔ suc ⁡ G ∈ On
72 70 71 sylib ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → suc ⁡ G ∈ On
73 eloni ⊢ suc ⁡ G ∈ On → Ord ⁡ suc ⁡ G
74 72 73 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 ∧ a ∈ suc ⁡ G → Ord ⁡ suc ⁡ G
75 simpr ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → a ∈ suc ⁡ G
76 ordsucss ⊢ Ord ⁡ suc ⁡ G → a ∈ suc ⁡ G → suc ⁡ a ⊆ suc ⁡ G
77 74 75 76 sylc ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → suc ⁡ a ⊆ suc ⁡ G
78 simpl33 ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → ∀ v ∈ B ¬ U < s v → U ↾ suc ⁡ G = v ↾ suc ⁡ G
79 reseq1 ⊢ U ↾ suc ⁡ G = v ↾ suc ⁡ G → U ↾ suc ⁡ G ↾ suc ⁡ a = v ↾ suc ⁡ G ↾ suc ⁡ a
80 resabs1 ⊢ suc ⁡ a ⊆ suc ⁡ G → U ↾ suc ⁡ G ↾ suc ⁡ a = U ↾ suc ⁡ a
81 resabs1 ⊢ suc ⁡ a ⊆ suc ⁡ G → v ↾ suc ⁡ G ↾ suc ⁡ a = v ↾ suc ⁡ a
82 80 81 eqeq12d ⊢ suc ⁡ a ⊆ suc ⁡ G → U ↾ suc ⁡ G ↾ suc ⁡ a = v ↾ suc ⁡ G ↾ suc ⁡ a ↔ U ↾ suc ⁡ a = v ↾ suc ⁡ a
83 79 82 syl5ib ⊢ suc ⁡ a ⊆ suc ⁡ G → U ↾ suc ⁡ G = v ↾ suc ⁡ G → U ↾ suc ⁡ a = v ↾ suc ⁡ a
84 83 imim2d ⊢ suc ⁡ a ⊆ suc ⁡ G → ¬ U < s v → U ↾ suc ⁡ G = v ↾ suc ⁡ G → ¬ U < s v → U ↾ suc ⁡ a = v ↾ suc ⁡ a
85 84 ralimdv ⊢ suc ⁡ a ⊆ suc ⁡ G → ∀ v ∈ B ¬ U < s v → U ↾ suc ⁡ G = v ↾ suc ⁡ G → ∀ v ∈ B ¬ U < s v → U ↾ suc ⁡ a = v ↾ suc ⁡ a
86 77 78 85 sylc ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → ∀ v ∈ B ¬ U < s v → U ↾ suc ⁡ a = v ↾ suc ⁡ a
87 1 noinffv ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ a ∈ dom ⁡ U ∧ ∀ v ∈ B ¬ U < s v → U ↾ suc ⁡ a = v ↾ suc ⁡ a → T ⁡ a = U ⁡ a
88 62 63 64 65 86 87 syl113anc ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → T ⁡ a = U ⁡ a
89 75 fvresd ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → T ↾ suc ⁡ G ⁡ a = T ⁡ a
90 75 fvresd ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → U ↾ suc ⁡ G ⁡ a = U ⁡ a
91 88 89 90 3eqtr4d ⊢ ¬ ∃ 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 ∧ a ∈ suc ⁡ G → T ↾ suc ⁡ G ⁡ a = U ↾ suc ⁡ G ⁡ a
92 91 ex ⊢ ¬ ∃ 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 → a ∈ suc ⁡ G → T ↾ suc ⁡ G ⁡ a = U ↾ suc ⁡ G ⁡ a
93 61 92 sylbid ⊢ ¬ ∃ 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 → a ∈ dom ⁡ T ↾ suc ⁡ G → T ↾ suc ⁡ G ⁡ a = U ↾ suc ⁡ G ⁡ a
94 93 ralrimiv ⊢ ¬ ∃ 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 → ∀ a ∈ dom ⁡ T ↾ suc ⁡ G T ↾ suc ⁡ G ⁡ a = U ↾ suc ⁡ G ⁡ a
95 nofun ⊢ T ∈ No → Fun ⁡ T
96 95 funresd ⊢ T ∈ No → Fun ⁡ T ↾ suc ⁡ G
97 4 96 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 → Fun ⁡ T ↾ suc ⁡ G
98 nofun ⊢ U ∈ No → Fun ⁡ U
99 98 funresd ⊢ U ∈ No → Fun ⁡ U ↾ suc ⁡ G
100 50 99 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 → Fun ⁡ U ↾ suc ⁡ G
101 eqfunfv ⊢ Fun ⁡ T ↾ suc ⁡ G ∧ Fun ⁡ U ↾ suc ⁡ G → T ↾ suc ⁡ G = U ↾ suc ⁡ G ↔ dom ⁡ T ↾ suc ⁡ G = dom ⁡ U ↾ suc ⁡ G ∧ ∀ a ∈ dom ⁡ T ↾ suc ⁡ G T ↾ suc ⁡ G ⁡ a = U ↾ suc ⁡ G ⁡ a
102 97 100 101 syl2anc ⊢ ¬ ∃ 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 → T ↾ suc ⁡ G = U ↾ suc ⁡ G ↔ dom ⁡ T ↾ suc ⁡ G = dom ⁡ U ↾ suc ⁡ G ∧ ∀ a ∈ dom ⁡ T ↾ suc ⁡ G T ↾ suc ⁡ G ⁡ a = U ↾ suc ⁡ G ⁡ a
103 60 94 102 mpbir2and ⊢ ¬ ∃ 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 → T ↾ suc ⁡ G = U ↾ suc ⁡ G