MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nosupbnd2 Structured version   Visualization version   GIF version

Theorem nosupbnd2 27080
Description: Bounding law from above for the surreal supremum. Proposition 4.3 of [Lipparini] p. 6. (Contributed by Scott Fenton, 6-Dec-2021.)
Hypothesis
Ref Expression
nosupbnd2.1 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
nosupbnd2 ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → (∀𝑎𝐴 𝑎 <s 𝑍 ↔ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆))
Distinct variable groups:   𝐴,𝑎,𝑔,𝑢,𝑣,𝑥,𝑦   𝑆,𝑎,𝑔   𝑣,𝑢,𝑥,𝑦   𝑍,𝑎,𝑔,𝑥
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑣,𝑢)   𝑍(𝑦,𝑣,𝑢)

Proof of Theorem nosupbnd2
Dummy variables 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1918 . . . . . 6 𝑥((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)
2 nfcv 2904 . . . . . . . . 9 𝑥𝑍
3 nosupbnd2.1 . . . . . . . . . . 11 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
4 nfre1 3267 . . . . . . . . . . . 12 𝑥𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦
5 nfriota1 7321 . . . . . . . . . . . . 13 𝑥(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
65nfdm 5907 . . . . . . . . . . . . . . 15 𝑥dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
7 nfcv 2904 . . . . . . . . . . . . . . 15 𝑥2o
86, 7nfop 4847 . . . . . . . . . . . . . 14 𝑥⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o
98nfsn 4669 . . . . . . . . . . . . 13 𝑥{⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}
105, 9nfun 4126 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})
11 nfcv 2904 . . . . . . . . . . . . 13 𝑥{𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
12 nfiota1 6451 . . . . . . . . . . . . 13 𝑥(℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
1311, 12nfmpt 5213 . . . . . . . . . . . 12 𝑥(𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
144, 10, 13nfif 4517 . . . . . . . . . . 11 𝑥if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
153, 14nfcxfr 2902 . . . . . . . . . 10 𝑥𝑆
1615nfdm 5907 . . . . . . . . 9 𝑥dom 𝑆
172, 16nfres 5940 . . . . . . . 8 𝑥(𝑍 ↾ dom 𝑆)
18 nfcv 2904 . . . . . . . 8 𝑥 <s
1917, 18, 15nfbr 5153 . . . . . . 7 𝑥(𝑍 ↾ dom 𝑆) <s 𝑆
2019nfn 1861 . . . . . 6 𝑥 ¬ (𝑍 ↾ dom 𝑆) <s 𝑆
211, 20nfim 1900 . . . . 5 𝑥(((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
22 simpl 484 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦))
23 rspe 3231 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2423adantr 482 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
25 nomaxmo 27062 . . . . . . . . . . . . 13 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
26253ad2ant1 1134 . . . . . . . . . . . 12 ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2726ad2antrl 727 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
28 reu5 3354 . . . . . . . . . . 11 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
2924, 27, 28sylanbrc 584 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
30 riota1 7336 . . . . . . . . . 10 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
3129, 30syl 17 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
3222, 31mpbid 231 . . . . . . . 8 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)
33 nosupbnd2lem1 27079 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {⟨dom 𝑥, 2o⟩}))
34333expb 1121 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {⟨dom 𝑥, 2o⟩}))
35 dmeq 5860 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = dom 𝑥)
36 suceq 6384 . . . . . . . . . . . . 13 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = dom 𝑥 → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = suc dom 𝑥)
3735, 36syl 17 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = suc dom 𝑥)
3837reseq2d 5938 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = (𝑍 ↾ suc dom 𝑥))
39 id 22 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)
4035opeq1d 4837 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩ = ⟨dom 𝑥, 2o⟩)
4140sneqd 4599 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩} = {⟨dom 𝑥, 2o⟩})
4239, 41uneq12d 4125 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (𝑥 ∪ {⟨dom 𝑥, 2o⟩}))
4338, 42breq12d 5119 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ((𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ↔ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {⟨dom 𝑥, 2o⟩})))
4443notbid 318 . . . . . . . . 9 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (¬ (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ↔ ¬ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {⟨dom 𝑥, 2o⟩})))
4534, 44syl5ibrcom 247 . . . . . . . 8 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ¬ (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})))
4632, 45mpd 15 . . . . . . 7 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
47 iftrue 4493 . . . . . . . . . . . . . 14 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
483, 47eqtrid 2785 . . . . . . . . . . . . 13 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
4923, 48syl 17 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → 𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
5049dmeqd 5862 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → dom 𝑆 = dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
51 2on 8427 . . . . . . . . . . . . . . 15 2o ∈ On
5251elexi 3463 . . . . . . . . . . . . . 14 2o ∈ V
5352dmsnop 6169 . . . . . . . . . . . . 13 dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩} = {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)}
5453uneq2i 4121 . . . . . . . . . . . 12 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
55 dmun 5867 . . . . . . . . . . . 12 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})
56 df-suc 6324 . . . . . . . . . . . 12 suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
5754, 55, 563eqtr4i 2771 . . . . . . . . . . 11 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
5850, 57eqtrdi 2789 . . . . . . . . . 10 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5958reseq2d 5938 . . . . . . . . 9 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → (𝑍 ↾ dom 𝑆) = (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)))
6059adantr 482 . . . . . . . 8 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑍 ↾ dom 𝑆) = (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)))
6149adantr 482 . . . . . . . 8 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
6260, 61breq12d 5119 . . . . . . 7 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ((𝑍 ↾ dom 𝑆) <s 𝑆 ↔ (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})))
6346, 62mtbird 325 . . . . . 6 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
6463exp31 421 . . . . 5 (𝑥𝐴 → (∀𝑦𝐴 ¬ 𝑥 <s 𝑦 → (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)))
6521, 64rexlimi 3241 . . . 4 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆))
6665imp 408 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
673nosupno 27067 . . . . . . . 8 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
68673adant3 1133 . . . . . . 7 ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → 𝑆 No )
6968ad2antrl 727 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝑆 No )
70 nodmon 27014 . . . . . . 7 (𝑆 No → dom 𝑆 ∈ On)
7169, 70syl 17 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → dom 𝑆 ∈ On)
72 noreson 27024 . . . . . 6 ((𝑆 No ∧ dom 𝑆 ∈ On) → (𝑆 ↾ dom 𝑆) ∈ No )
7369, 71, 72syl2anc 585 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑆 ↾ dom 𝑆) ∈ No )
74 simprl3 1221 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝑍 No )
75 noreson 27024 . . . . . 6 ((𝑍 No ∧ dom 𝑆 ∈ On) → (𝑍 ↾ dom 𝑆) ∈ No )
7674, 71, 75syl2anc 585 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑍 ↾ dom 𝑆) ∈ No )
77 dmres 5960 . . . . . . 7 dom (𝑆 ↾ dom 𝑆) = (dom 𝑆 ∩ dom 𝑆)
78 inss2 4190 . . . . . . 7 (dom 𝑆 ∩ dom 𝑆) ⊆ dom 𝑆
7977, 78eqsstri 3979 . . . . . 6 dom (𝑆 ↾ dom 𝑆) ⊆ dom 𝑆
8079a1i 11 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → dom (𝑆 ↾ dom 𝑆) ⊆ dom 𝑆)
81 dmres 5960 . . . . . . 7 dom (𝑍 ↾ dom 𝑆) = (dom 𝑆 ∩ dom 𝑍)
82 inss1 4189 . . . . . . 7 (dom 𝑆 ∩ dom 𝑍) ⊆ dom 𝑆
8381, 82eqsstri 3979 . . . . . 6 dom (𝑍 ↾ dom 𝑆) ⊆ dom 𝑆
8483a1i 11 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → dom (𝑍 ↾ dom 𝑆) ⊆ dom 𝑆)
853nosupdm 27068 . . . . . . . . . . 11 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑔 ∣ ∃𝑝𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))})
8685eqabd 2877 . . . . . . . . . 10 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑔 ∈ dom 𝑆 ↔ ∃𝑝𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
8786adantr 482 . . . . . . . . 9 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑔 ∈ dom 𝑆 ↔ ∃𝑝𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
88 simprl 770 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝𝐴)
89 simplrr 777 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑎𝐴 𝑎 <s 𝑍)
90 breq1 5109 . . . . . . . . . . . . . . 15 (𝑎 = 𝑝 → (𝑎 <s 𝑍𝑝 <s 𝑍))
9190rspcv 3576 . . . . . . . . . . . . . 14 (𝑝𝐴 → (∀𝑎𝐴 𝑎 <s 𝑍𝑝 <s 𝑍))
9288, 89, 91sylc 65 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 <s 𝑍)
93 simprl1 1219 . . . . . . . . . . . . . . . 16 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝐴 No )
9493adantr 482 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐴 No )
9594, 88sseldd 3946 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 No )
9674adantr 482 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 No )
97 sltso 27040 . . . . . . . . . . . . . . 15 <s Or No
98 soasym 5577 . . . . . . . . . . . . . . 15 (( <s Or No ∧ (𝑝 No 𝑍 No )) → (𝑝 <s 𝑍 → ¬ 𝑍 <s 𝑝))
9997, 98mpan 689 . . . . . . . . . . . . . 14 ((𝑝 No 𝑍 No ) → (𝑝 <s 𝑍 → ¬ 𝑍 <s 𝑝))
10095, 96, 99syl2anc 585 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝑝 <s 𝑍 → ¬ 𝑍 <s 𝑝))
10192, 100mpd 15 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ 𝑍 <s 𝑝)
102 nodmon 27014 . . . . . . . . . . . . . . . 16 (𝑝 No → dom 𝑝 ∈ On)
10395, 102syl 17 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → dom 𝑝 ∈ On)
104 simprrl 780 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ dom 𝑝)
105 onelon 6343 . . . . . . . . . . . . . . 15 ((dom 𝑝 ∈ On ∧ 𝑔 ∈ dom 𝑝) → 𝑔 ∈ On)
106103, 104, 105syl2anc 585 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ On)
107 onsucb 7753 . . . . . . . . . . . . . 14 (𝑔 ∈ On ↔ suc 𝑔 ∈ On)
108106, 107sylib 217 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → suc 𝑔 ∈ On)
109 sltres 27026 . . . . . . . . . . . . 13 ((𝑍 No 𝑝 No ∧ suc 𝑔 ∈ On) → ((𝑍 ↾ suc 𝑔) <s (𝑝 ↾ suc 𝑔) → 𝑍 <s 𝑝))
11096, 95, 108, 109syl3anc 1372 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ((𝑍 ↾ suc 𝑔) <s (𝑝 ↾ suc 𝑔) → 𝑍 <s 𝑝))
111101, 110mtod 197 . . . . . . . . . . 11 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑝 ↾ suc 𝑔))
112 simpll 766 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
113 simprl2 1220 . . . . . . . . . . . . . . 15 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝐴 ∈ V)
11493, 113jca 513 . . . . . . . . . . . . . 14 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝐴 No 𝐴 ∈ V))
115114adantr 482 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝐴 No 𝐴 ∈ V))
116 simprrr 781 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
117 breq1 5109 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑞 → (𝑣 <s 𝑝𝑞 <s 𝑝))
118117notbid 318 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑞 → (¬ 𝑣 <s 𝑝 ↔ ¬ 𝑞 <s 𝑝))
119 reseq1 5932 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑞 → (𝑣 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))
120119eqeq2d 2744 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑞 → ((𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔) ↔ (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
121118, 120imbi12d 345 . . . . . . . . . . . . . . 15 (𝑣 = 𝑞 → ((¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))
122121cbvralvw 3224 . . . . . . . . . . . . . 14 (∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
123116, 122sylibr 233 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
1243nosupres 27071 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑝𝐴𝑔 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (𝑆 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔))
125112, 115, 88, 104, 123, 124syl113anc 1383 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝑆 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔))
126125breq2d 5118 . . . . . . . . . . 11 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ((𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔) ↔ (𝑍 ↾ suc 𝑔) <s (𝑝 ↾ suc 𝑔)))
127111, 126mtbird 325 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔))
128127rexlimdvaa 3150 . . . . . . . . 9 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (∃𝑝𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔)))
12987, 128sylbid 239 . . . . . . . 8 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑔 ∈ dom 𝑆 → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔)))
130129imp 408 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔))
13169adantr 482 . . . . . . . . . . 11 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → 𝑆 No )
132 nodmord 27017 . . . . . . . . . . 11 (𝑆 No → Ord dom 𝑆)
133131, 132syl 17 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → Ord dom 𝑆)
134 simpr 486 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → 𝑔 ∈ dom 𝑆)
135 ordsucss 7754 . . . . . . . . . 10 (Ord dom 𝑆 → (𝑔 ∈ dom 𝑆 → suc 𝑔 ⊆ dom 𝑆))
136133, 134, 135sylc 65 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → suc 𝑔 ⊆ dom 𝑆)
137136resabs1d 5969 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) = (𝑍 ↾ suc 𝑔))
138136resabs1d 5969 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔) = (𝑆 ↾ suc 𝑔))
139137, 138breq12d 5119 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → (((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) <s ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔) ↔ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔)))
140130, 139mtbird 325 . . . . . 6 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ¬ ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) <s ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔))
141140ralrimiva 3140 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ∀𝑔 ∈ dom 𝑆 ¬ ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) <s ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔))
142 noresle 27061 . . . . 5 ((((𝑆 ↾ dom 𝑆) ∈ No ∧ (𝑍 ↾ dom 𝑆) ∈ No ) ∧ (dom (𝑆 ↾ dom 𝑆) ⊆ dom 𝑆 ∧ dom (𝑍 ↾ dom 𝑆) ⊆ dom 𝑆 ∧ ∀𝑔 ∈ dom 𝑆 ¬ ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) <s ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔))) → ¬ (𝑍 ↾ dom 𝑆) <s (𝑆 ↾ dom 𝑆))
14373, 76, 80, 84, 141, 142syl23anc 1378 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s (𝑆 ↾ dom 𝑆))
144 nofun 27013 . . . . . . 7 (𝑆 No → Fun 𝑆)
14569, 144syl 17 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → Fun 𝑆)
146 funrel 6519 . . . . . 6 (Fun 𝑆 → Rel 𝑆)
147 resdm 5983 . . . . . 6 (Rel 𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆)
148145, 146, 1473syl 18 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑆 ↾ dom 𝑆) = 𝑆)
149148breq2d 5118 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ((𝑍 ↾ dom 𝑆) <s (𝑆 ↾ dom 𝑆) ↔ (𝑍 ↾ dom 𝑆) <s 𝑆))
150143, 149mtbid 324 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
15166, 150pm2.61ian 811 . 2 (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
152 simpll1 1213 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝐴 No )
153 simpll2 1214 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝐴 ∈ V)
154 simpr 486 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑎𝐴)
1553nosupbnd1 27078 . . . . . 6 ((𝐴 No 𝐴 ∈ V ∧ 𝑎𝐴) → (𝑎 ↾ dom 𝑆) <s 𝑆)
156152, 153, 154, 155syl3anc 1372 . . . . 5 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (𝑎 ↾ dom 𝑆) <s 𝑆)
157 simplr 768 . . . . 5 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
158 simpl1 1192 . . . . . . . 8 (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → 𝐴 No )
159158sselda 3945 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑎 No )
160152, 153, 67syl2anc 585 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑆 No )
161160, 70syl 17 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → dom 𝑆 ∈ On)
162 noreson 27024 . . . . . . 7 ((𝑎 No ∧ dom 𝑆 ∈ On) → (𝑎 ↾ dom 𝑆) ∈ No )
163159, 161, 162syl2anc 585 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (𝑎 ↾ dom 𝑆) ∈ No )
164 simpll3 1215 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑍 No )
165164, 161, 75syl2anc 585 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (𝑍 ↾ dom 𝑆) ∈ No )
166 sotr3 5585 . . . . . . 7 (( <s Or No ∧ ((𝑎 ↾ dom 𝑆) ∈ No 𝑆 No ∧ (𝑍 ↾ dom 𝑆) ∈ No )) → (((𝑎 ↾ dom 𝑆) <s 𝑆 ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆)))
16797, 166mpan 689 . . . . . 6 (((𝑎 ↾ dom 𝑆) ∈ No 𝑆 No ∧ (𝑍 ↾ dom 𝑆) ∈ No ) → (((𝑎 ↾ dom 𝑆) <s 𝑆 ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆)))
168163, 160, 165, 167syl3anc 1372 . . . . 5 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (((𝑎 ↾ dom 𝑆) <s 𝑆 ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆)))
169156, 157, 168mp2and 698 . . . 4 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆))
170 sltres 27026 . . . . 5 ((𝑎 No 𝑍 No ∧ dom 𝑆 ∈ On) → ((𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆) → 𝑎 <s 𝑍))
171159, 164, 161, 170syl3anc 1372 . . . 4 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → ((𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆) → 𝑎 <s 𝑍))
172169, 171mpd 15 . . 3 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑎 <s 𝑍)
173172ralrimiva 3140 . 2 (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → ∀𝑎𝐴 𝑎 <s 𝑍)
174151, 173impbida 800 1 ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → (∀𝑎𝐴 𝑎 <s 𝑍 ↔ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  {cab 2710  wral 3061  wrex 3070  ∃!wreu 3350  ∃*wrmo 3351  Vcvv 3444  cun 3909  cin 3910  wss 3911  ifcif 4487  {csn 4587  cop 4593   class class class wbr 5106  cmpt 5189   Or wor 5545  dom cdm 5634  cres 5636  Rel wrel 5639  Ord word 6317  Oncon0 6318  suc csuc 6320  cio 6447  Fun wfun 6491  cfv 6497  crio 7313  2oc2o 8407   No csur 27004   <s cslt 27005
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-ord 6321  df-on 6322  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-1o 8413  df-2o 8414  df-no 27007  df-slt 27008  df-bday 27009
This theorem is referenced by:  nosupinfsep  27096  noetasuplem4  27100
  Copyright terms: Public domain W3C validator