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

Theorem nosupbnd2 27762
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 1913 . . . . . 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 3284 . . . . . . . . . . . 12 𝑥𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦
5 nfriota1 7396 . . . . . . . . . . . . 13 𝑥(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
65nfdm 5961 . . . . . . . . . . . . . . 15 𝑥dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
7 nfcv 2904 . . . . . . . . . . . . . . 15 𝑥2o
86, 7nfop 4888 . . . . . . . . . . . . . 14 𝑥⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o
98nfsn 4706 . . . . . . . . . . . . 13 𝑥{⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}
105, 9nfun 4169 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})
11 nfcv 2904 . . . . . . . . . . . . 13 𝑥{𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
12 nfiota1 6515 . . . . . . . . . . . . 13 𝑥(℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
1311, 12nfmpt 5248 . . . . . . . . . . . 12 𝑥(𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
144, 10, 13nfif 4555 . . . . . . . . . . 11 𝑥if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
153, 14nfcxfr 2902 . . . . . . . . . 10 𝑥𝑆
1615nfdm 5961 . . . . . . . . 9 𝑥dom 𝑆
172, 16nfres 5998 . . . . . . . 8 𝑥(𝑍 ↾ dom 𝑆)
18 nfcv 2904 . . . . . . . 8 𝑥 <s
1917, 18, 15nfbr 5189 . . . . . . 7 𝑥(𝑍 ↾ dom 𝑆) <s 𝑆
2019nfn 1856 . . . . . 6 𝑥 ¬ (𝑍 ↾ dom 𝑆) <s 𝑆
211, 20nfim 1895 . . . . 5 𝑥(((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
22 simpl 482 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦))
23 rspe 3248 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2423adantr 480 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
25 nomaxmo 27744 . . . . . . . . . . . . 13 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
26253ad2ant1 1133 . . . . . . . . . . . 12 ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2726ad2antrl 728 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
28 reu5 3381 . . . . . . . . . . 11 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
2924, 27, 28sylanbrc 583 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
30 riota1 7410 . . . . . . . . . 10 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
3129, 30syl 17 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
3222, 31mpbid 232 . . . . . . . 8 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)
33 nosupbnd2lem1 27761 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {⟨dom 𝑥, 2o⟩}))
34333expb 1120 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {⟨dom 𝑥, 2o⟩}))
35 dmeq 5913 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = dom 𝑥)
36 suceq 6449 . . . . . . . . . . . . 13 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = dom 𝑥 → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = suc dom 𝑥)
3735, 36syl 17 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = suc dom 𝑥)
3837reseq2d 5996 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = (𝑍 ↾ suc dom 𝑥))
39 id 22 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)
4035opeq1d 4878 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩ = ⟨dom 𝑥, 2o⟩)
4140sneqd 4637 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩} = {⟨dom 𝑥, 2o⟩})
4239, 41uneq12d 4168 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (𝑥 ∪ {⟨dom 𝑥, 2o⟩}))
4338, 42breq12d 5155 . . . . . . . . . 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 4530 . . . . . . . . . . . . . 14 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
483, 47eqtrid 2788 . . . . . . . . . . . . 13 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
4923, 48syl 17 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → 𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
5049dmeqd 5915 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → dom 𝑆 = dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
51 2on 8521 . . . . . . . . . . . . . . 15 2o ∈ On
5251elexi 3502 . . . . . . . . . . . . . 14 2o ∈ V
5352dmsnop 6235 . . . . . . . . . . . . 13 dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩} = {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)}
5453uneq2i 4164 . . . . . . . . . . . 12 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
55 dmun 5920 . . . . . . . . . . . 12 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})
56 df-suc 6389 . . . . . . . . . . . 12 suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
5754, 55, 563eqtr4i 2774 . . . . . . . . . . 11 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
5850, 57eqtrdi 2792 . . . . . . . . . 10 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5958reseq2d 5996 . . . . . . . . 9 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → (𝑍 ↾ dom 𝑆) = (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)))
6059adantr 480 . . . . . . . 8 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑍 ↾ dom 𝑆) = (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)))
6149adantr 480 . . . . . . . 8 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
6260, 61breq12d 5155 . . . . . . 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 419 . . . . 5 (𝑥𝐴 → (∀𝑦𝐴 ¬ 𝑥 <s 𝑦 → (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)))
6521, 64rexlimi 3258 . . . 4 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆))
6665imp 406 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
673nosupno 27749 . . . . . . . 8 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
68673adant3 1132 . . . . . . 7 ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → 𝑆 No )
6968ad2antrl 728 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝑆 No )
70 nodmon 27696 . . . . . . 7 (𝑆 No → dom 𝑆 ∈ On)
7169, 70syl 17 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → dom 𝑆 ∈ On)
72 noreson 27706 . . . . . 6 ((𝑆 No ∧ dom 𝑆 ∈ On) → (𝑆 ↾ dom 𝑆) ∈ No )
7369, 71, 72syl2anc 584 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑆 ↾ dom 𝑆) ∈ No )
74 simprl3 1220 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝑍 No )
75 noreson 27706 . . . . . 6 ((𝑍 No ∧ dom 𝑆 ∈ On) → (𝑍 ↾ dom 𝑆) ∈ No )
7674, 71, 75syl2anc 584 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑍 ↾ dom 𝑆) ∈ No )
77 dmres 6029 . . . . . . 7 dom (𝑆 ↾ dom 𝑆) = (dom 𝑆 ∩ dom 𝑆)
78 inss2 4237 . . . . . . 7 (dom 𝑆 ∩ dom 𝑆) ⊆ dom 𝑆
7977, 78eqsstri 4029 . . . . . 6 dom (𝑆 ↾ dom 𝑆) ⊆ dom 𝑆
8079a1i 11 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → dom (𝑆 ↾ dom 𝑆) ⊆ dom 𝑆)
81 dmres 6029 . . . . . . 7 dom (𝑍 ↾ dom 𝑆) = (dom 𝑆 ∩ dom 𝑍)
82 inss1 4236 . . . . . . 7 (dom 𝑆 ∩ dom 𝑍) ⊆ dom 𝑆
8381, 82eqsstri 4029 . . . . . 6 dom (𝑍 ↾ dom 𝑆) ⊆ dom 𝑆
8483a1i 11 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → dom (𝑍 ↾ dom 𝑆) ⊆ dom 𝑆)
853nosupdm 27750 . . . . . . . . . . 11 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑔 ∣ ∃𝑝𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))})
8685eqabrd 2883 . . . . . . . . . 10 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑔 ∈ dom 𝑆 ↔ ∃𝑝𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
8786adantr 480 . . . . . . . . 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 5145 . . . . . . . . . . . . . . 15 (𝑎 = 𝑝 → (𝑎 <s 𝑍𝑝 <s 𝑍))
9190rspcv 3617 . . . . . . . . . . . . . 14 (𝑝𝐴 → (∀𝑎𝐴 𝑎 <s 𝑍𝑝 <s 𝑍))
9288, 89, 91sylc 65 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 <s 𝑍)
93 simprl1 1218 . . . . . . . . . . . . . . . 16 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝐴 No )
9493adantr 480 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐴 No )
9594, 88sseldd 3983 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 No )
9674adantr 480 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 No )
97 sltso 27722 . . . . . . . . . . . . . . 15 <s Or No
98 soasym 5624 . . . . . . . . . . . . . . 15 (( <s Or No ∧ (𝑝 No 𝑍 No )) → (𝑝 <s 𝑍 → ¬ 𝑍 <s 𝑝))
9997, 98mpan 690 . . . . . . . . . . . . . 14 ((𝑝 No 𝑍 No ) → (𝑝 <s 𝑍 → ¬ 𝑍 <s 𝑝))
10095, 96, 99syl2anc 584 . . . . . . . . . . . . 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 27696 . . . . . . . . . . . . . . . 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 6408 . . . . . . . . . . . . . . 15 ((dom 𝑝 ∈ On ∧ 𝑔 ∈ dom 𝑝) → 𝑔 ∈ On)
106103, 104, 105syl2anc 584 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ On)
107 onsucb 7838 . . . . . . . . . . . . . 14 (𝑔 ∈ On ↔ suc 𝑔 ∈ On)
108106, 107sylib 218 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → suc 𝑔 ∈ On)
109 sltres 27708 . . . . . . . . . . . . 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 198 . . . . . . . . . . 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 1219 . . . . . . . . . . . . . . 15 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝐴 ∈ V)
11493, 113jca 511 . . . . . . . . . . . . . 14 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝐴 No 𝐴 ∈ V))
115114adantr 480 . . . . . . . . . . . . 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 5145 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑞 → (𝑣 <s 𝑝𝑞 <s 𝑝))
118117notbid 318 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑞 → (¬ 𝑣 <s 𝑝 ↔ ¬ 𝑞 <s 𝑝))
119 reseq1 5990 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑞 → (𝑣 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))
120119eqeq2d 2747 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑞 → ((𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔) ↔ (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
121118, 120imbi12d 344 . . . . . . . . . . . . . . 15 (𝑣 = 𝑞 → ((¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))
122121cbvralvw 3236 . . . . . . . . . . . . . 14 (∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
123116, 122sylibr 234 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
1243nosupres 27753 . . . . . . . . . . . . 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 5154 . . . . . . . . . . 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 3155 . . . . . . . . 9 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (∃𝑝𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔)))
12987, 128sylbid 240 . . . . . . . 8 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑔 ∈ dom 𝑆 → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔)))
130129imp 406 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔))
13169adantr 480 . . . . . . . . . . 11 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → 𝑆 No )
132 nodmord 27699 . . . . . . . . . . 11 (𝑆 No → Ord dom 𝑆)
133131, 132syl 17 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → Ord dom 𝑆)
134 simpr 484 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → 𝑔 ∈ dom 𝑆)
135 ordsucss 7839 . . . . . . . . . 10 (Ord dom 𝑆 → (𝑔 ∈ dom 𝑆 → suc 𝑔 ⊆ dom 𝑆))
136133, 134, 135sylc 65 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → suc 𝑔 ⊆ dom 𝑆)
137136resabs1d 6025 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) = (𝑍 ↾ suc 𝑔))
138136resabs1d 6025 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔) = (𝑆 ↾ suc 𝑔))
139137, 138breq12d 5155 . . . . . . 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 3145 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ∀𝑔 ∈ dom 𝑆 ¬ ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) <s ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔))
142 noresle 27743 . . . . 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 27695 . . . . . 6 (𝑆 No → Fun 𝑆)
145 funrel 6582 . . . . . 6 (Fun 𝑆 → Rel 𝑆)
146 resdm 6043 . . . . . 6 (Rel 𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆)
14769, 144, 145, 1464syl 19 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑆 ↾ dom 𝑆) = 𝑆)
148147breq2d 5154 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ((𝑍 ↾ dom 𝑆) <s (𝑆 ↾ dom 𝑆) ↔ (𝑍 ↾ dom 𝑆) <s 𝑆))
149143, 148mtbid 324 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
15066, 149pm2.61ian 811 . 2 (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
151 simpll1 1212 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝐴 No )
152 simpll2 1213 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝐴 ∈ V)
153 simpr 484 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑎𝐴)
1543nosupbnd1 27760 . . . . . 6 ((𝐴 No 𝐴 ∈ V ∧ 𝑎𝐴) → (𝑎 ↾ dom 𝑆) <s 𝑆)
155151, 152, 153, 154syl3anc 1372 . . . . 5 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (𝑎 ↾ dom 𝑆) <s 𝑆)
156 simplr 768 . . . . 5 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
157 simpl1 1191 . . . . . . . 8 (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → 𝐴 No )
158157sselda 3982 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑎 No )
159151, 152, 67syl2anc 584 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑆 No )
160159, 70syl 17 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → dom 𝑆 ∈ On)
161 noreson 27706 . . . . . . 7 ((𝑎 No ∧ dom 𝑆 ∈ On) → (𝑎 ↾ dom 𝑆) ∈ No )
162158, 160, 161syl2anc 584 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (𝑎 ↾ dom 𝑆) ∈ No )
163 simpll3 1214 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑍 No )
164163, 160, 75syl2anc 584 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (𝑍 ↾ dom 𝑆) ∈ No )
165 sotr3 5632 . . . . . . 7 (( <s Or No ∧ ((𝑎 ↾ dom 𝑆) ∈ No 𝑆 No ∧ (𝑍 ↾ dom 𝑆) ∈ No )) → (((𝑎 ↾ dom 𝑆) <s 𝑆 ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆)))
16697, 165mpan 690 . . . . . 6 (((𝑎 ↾ dom 𝑆) ∈ No 𝑆 No ∧ (𝑍 ↾ dom 𝑆) ∈ No ) → (((𝑎 ↾ dom 𝑆) <s 𝑆 ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆)))
167162, 159, 164, 166syl3anc 1372 . . . . 5 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (((𝑎 ↾ dom 𝑆) <s 𝑆 ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆)))
168155, 156, 167mp2and 699 . . . 4 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆))
169 sltres 27708 . . . . 5 ((𝑎 No 𝑍 No ∧ dom 𝑆 ∈ On) → ((𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆) → 𝑎 <s 𝑍))
170158, 163, 160, 169syl3anc 1372 . . . 4 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → ((𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆) → 𝑎 <s 𝑍))
171168, 170mpd 15 . . 3 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑎 <s 𝑍)
172171ralrimiva 3145 . 2 (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → ∀𝑎𝐴 𝑎 <s 𝑍)
173150, 172impbida 800 1 ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → (∀𝑎𝐴 𝑎 <s 𝑍 ↔ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1539  wcel 2107  {cab 2713  wral 3060  wrex 3069  ∃!wreu 3377  ∃*wrmo 3378  Vcvv 3479  cun 3948  cin 3949  wss 3950  ifcif 4524  {csn 4625  cop 4631   class class class wbr 5142  cmpt 5224   Or wor 5590  dom cdm 5684  cres 5686  Rel wrel 5689  Ord word 6382  Oncon0 6383  suc csuc 6385  cio 6511  Fun wfun 6554  cfv 6560  crio 7388  2oc2o 8501   No csur 27685   <s cslt 27686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4907  df-int 4946  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-ord 6386  df-on 6387  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-1o 8507  df-2o 8508  df-no 27688  df-slt 27689  df-bday 27690
This theorem is referenced by:  nosupinfsep  27778  noetasuplem4  27782
  Copyright terms: Public domain W3C validator