Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nosupbnd2 Structured version   Visualization version   GIF version

Theorem nosupbnd2 33100
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 1908 . . . . . 6 𝑥((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)
2 nfcv 2982 . . . . . . . . 9 𝑥𝑍
3 nosupbnd2.1 . . . . . . . . . . 11 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
4 nfre1 3311 . . . . . . . . . . . 12 𝑥𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦
5 nfriota1 7113 . . . . . . . . . . . . 13 𝑥(𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
65nfdm 5822 . . . . . . . . . . . . . . 15 𝑥dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
7 nfcv 2982 . . . . . . . . . . . . . . 15 𝑥2o
86, 7nfop 4818 . . . . . . . . . . . . . 14 𝑥⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o
98nfsn 4642 . . . . . . . . . . . . 13 𝑥{⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}
105, 9nfun 4145 . . . . . . . . . . . 12 𝑥((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})
11 nfcv 2982 . . . . . . . . . . . . 13 𝑥{𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
12 nfiota1 6314 . . . . . . . . . . . . 13 𝑥(℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
1311, 12nfmpt 5160 . . . . . . . . . . . 12 𝑥(𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
144, 10, 13nfif 4499 . . . . . . . . . . 11 𝑥if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
153, 14nfcxfr 2980 . . . . . . . . . 10 𝑥𝑆
1615nfdm 5822 . . . . . . . . 9 𝑥dom 𝑆
172, 16nfres 5854 . . . . . . . 8 𝑥(𝑍 ↾ dom 𝑆)
18 nfcv 2982 . . . . . . . 8 𝑥 <s
1917, 18, 15nfbr 5110 . . . . . . 7 𝑥(𝑍 ↾ dom 𝑆) <s 𝑆
2019nfn 1850 . . . . . 6 𝑥 ¬ (𝑍 ↾ dom 𝑆) <s 𝑆
211, 20nfim 1890 . . . . 5 𝑥(((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
22 simpl 483 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦))
23 rspe 3309 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2423adantr 481 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
25 nomaxmo 33085 . . . . . . . . . . . . 13 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
26253ad2ant1 1127 . . . . . . . . . . . 12 ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2726ad2antrl 724 . . . . . . . . . . 11 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
28 reu5 3436 . . . . . . . . . . 11 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
2924, 27, 28sylanbrc 583 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
30 riota1 7127 . . . . . . . . . 10 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
3129, 30syl 17 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ↔ (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥))
3222, 31mpbid 233 . . . . . . . 8 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)
33 nosupbnd2lem1 33099 . . . . . . . . . 10 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ (𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {⟨dom 𝑥, 2o⟩}))
34333expb 1114 . . . . . . . . 9 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {⟨dom 𝑥, 2o⟩}))
35 dmeq 5771 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = dom 𝑥)
36 suceq 6254 . . . . . . . . . . . . 13 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = dom 𝑥 → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = suc dom 𝑥)
3735, 36syl 17 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = suc dom 𝑥)
3837reseq2d 5852 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) = (𝑍 ↾ suc dom 𝑥))
39 id 22 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥)
4035opeq1d 4808 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩ = ⟨dom 𝑥, 2o⟩)
4140sneqd 4576 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩} = {⟨dom 𝑥, 2o⟩})
4239, 41uneq12d 4144 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (𝑥 ∪ {⟨dom 𝑥, 2o⟩}))
4338, 42breq12d 5076 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → ((𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ↔ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {⟨dom 𝑥, 2o⟩})))
4443notbid 319 . . . . . . . . 9 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = 𝑥 → (¬ (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ↔ ¬ (𝑍 ↾ suc dom 𝑥) <s (𝑥 ∪ {⟨dom 𝑥, 2o⟩})))
4534, 44syl5ibrcom 248 . . . . . . . 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 4476 . . . . . . . . . . . . . 14 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
483, 47syl5eq 2873 . . . . . . . . . . . . 13 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
4923, 48syl 17 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → 𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
5049dmeqd 5773 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → dom 𝑆 = dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
51 2on 8102 . . . . . . . . . . . . . . 15 2o ∈ On
5251elexi 3519 . . . . . . . . . . . . . 14 2o ∈ V
5352dmsnop 6071 . . . . . . . . . . . . 13 dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩} = {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)}
5453uneq2i 4140 . . . . . . . . . . . 12 (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
55 dmun 5778 . . . . . . . . . . . 12 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})
56 df-suc 6195 . . . . . . . . . . . 12 suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) = (dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)})
5754, 55, 563eqtr4i 2859 . . . . . . . . . . 11 dom ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
5850, 57syl6eq 2877 . . . . . . . . . 10 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → dom 𝑆 = suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
5958reseq2d 5852 . . . . . . . . 9 ((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) → (𝑍 ↾ dom 𝑆) = (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)))
6059adantr 481 . . . . . . . 8 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑍 ↾ dom 𝑆) = (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)))
6149adantr 481 . . . . . . . 8 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝑆 = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
6260, 61breq12d 5076 . . . . . . 7 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ((𝑍 ↾ dom 𝑆) <s 𝑆 ↔ (𝑍 ↾ suc dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)) <s ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩})))
6346, 62mtbird 326 . . . . . 6 (((𝑥𝐴 ∧ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦) ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
6463exp31 420 . . . . 5 (𝑥𝐴 → (∀𝑦𝐴 ¬ 𝑥 <s 𝑦 → (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)))
6521, 64rexlimi 3320 . . . 4 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆))
6665imp 407 . . 3 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
673nosupno 33087 . . . . . . . 8 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
68673adant3 1126 . . . . . . 7 ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → 𝑆 No )
6968ad2antrl 724 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝑆 No )
70 nodmon 33041 . . . . . . 7 (𝑆 No → dom 𝑆 ∈ On)
7169, 70syl 17 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → dom 𝑆 ∈ On)
72 noreson 33051 . . . . . 6 ((𝑆 No ∧ dom 𝑆 ∈ On) → (𝑆 ↾ dom 𝑆) ∈ No )
7369, 71, 72syl2anc 584 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑆 ↾ dom 𝑆) ∈ No )
74 simprl3 1214 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝑍 No )
75 noreson 33051 . . . . . 6 ((𝑍 No ∧ dom 𝑆 ∈ On) → (𝑍 ↾ dom 𝑆) ∈ No )
7674, 71, 75syl2anc 584 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑍 ↾ dom 𝑆) ∈ No )
77 dmres 5874 . . . . . . 7 dom (𝑆 ↾ dom 𝑆) = (dom 𝑆 ∩ dom 𝑆)
78 inss2 4210 . . . . . . 7 (dom 𝑆 ∩ dom 𝑆) ⊆ dom 𝑆
7977, 78eqsstri 4005 . . . . . 6 dom (𝑆 ↾ dom 𝑆) ⊆ dom 𝑆
8079a1i 11 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → dom (𝑆 ↾ dom 𝑆) ⊆ dom 𝑆)
81 dmres 5874 . . . . . . 7 dom (𝑍 ↾ dom 𝑆) = (dom 𝑆 ∩ dom 𝑍)
82 inss1 4209 . . . . . . 7 (dom 𝑆 ∩ dom 𝑍) ⊆ dom 𝑆
8381, 82eqsstri 4005 . . . . . 6 dom (𝑍 ↾ dom 𝑆) ⊆ dom 𝑆
8483a1i 11 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → dom (𝑍 ↾ dom 𝑆) ⊆ dom 𝑆)
853nosupdm 33088 . . . . . . . . . . 11 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑔 ∣ ∃𝑝𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))})
8685abeq2d 2952 . . . . . . . . . 10 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑔 ∈ dom 𝑆 ↔ ∃𝑝𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
8786adantr 481 . . . . . . . . 9 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑔 ∈ dom 𝑆 ↔ ∃𝑝𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))))
88 simprl 767 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝𝐴)
89 simplrr 774 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑎𝐴 𝑎 <s 𝑍)
90 breq1 5066 . . . . . . . . . . . . . . 15 (𝑎 = 𝑝 → (𝑎 <s 𝑍𝑝 <s 𝑍))
9190rspcv 3622 . . . . . . . . . . . . . 14 (𝑝𝐴 → (∀𝑎𝐴 𝑎 <s 𝑍𝑝 <s 𝑍))
9288, 89, 91sylc 65 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 <s 𝑍)
93 simprl1 1212 . . . . . . . . . . . . . . . 16 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝐴 No )
9493adantr 481 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝐴 No )
9594, 88sseldd 3972 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑝 No )
9674adantr 481 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑍 No )
97 sltso 33065 . . . . . . . . . . . . . . 15 <s Or No
98 soasym 5503 . . . . . . . . . . . . . . 15 (( <s Or No ∧ (𝑝 No 𝑍 No )) → (𝑝 <s 𝑍 → ¬ 𝑍 <s 𝑝))
9997, 98mpan 686 . . . . . . . . . . . . . 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 33041 . . . . . . . . . . . . . . . 16 (𝑝 No → dom 𝑝 ∈ On)
10395, 102syl 17 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → dom 𝑝 ∈ On)
104 simprrl 777 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ dom 𝑝)
105 onelon 6214 . . . . . . . . . . . . . . 15 ((dom 𝑝 ∈ On ∧ 𝑔 ∈ dom 𝑝) → 𝑔 ∈ On)
106103, 104, 105syl2anc 584 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → 𝑔 ∈ On)
107 sucelon 7520 . . . . . . . . . . . . . 14 (𝑔 ∈ On ↔ suc 𝑔 ∈ On)
108106, 107sylib 219 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → suc 𝑔 ∈ On)
109 sltres 33053 . . . . . . . . . . . . 13 ((𝑍 No 𝑝 No ∧ suc 𝑔 ∈ On) → ((𝑍 ↾ suc 𝑔) <s (𝑝 ↾ suc 𝑔) → 𝑍 <s 𝑝))
11096, 95, 108, 109syl3anc 1365 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ((𝑍 ↾ suc 𝑔) <s (𝑝 ↾ suc 𝑔) → 𝑍 <s 𝑝))
111101, 110mtod 199 . . . . . . . . . . 11 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑝 ↾ suc 𝑔))
112 simpll 763 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
113 simprl2 1213 . . . . . . . . . . . . . . 15 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → 𝐴 ∈ V)
11493, 113jca 512 . . . . . . . . . . . . . 14 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝐴 No 𝐴 ∈ V))
115114adantr 481 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝐴 No 𝐴 ∈ V))
116 simprrr 778 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
117 breq1 5066 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑞 → (𝑣 <s 𝑝𝑞 <s 𝑝))
118117notbid 319 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑞 → (¬ 𝑣 <s 𝑝 ↔ ¬ 𝑞 <s 𝑝))
119 reseq1 5846 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑞 → (𝑣 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))
120119eqeq2d 2837 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑞 → ((𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔) ↔ (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
121118, 120imbi12d 346 . . . . . . . . . . . . . . 15 (𝑣 = 𝑞 → ((¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))
122121cbvralv 3458 . . . . . . . . . . . . . 14 (∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔)))
123116, 122sylibr 235 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
1243nosupres 33091 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑝𝐴𝑔 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (𝑆 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔))
125112, 115, 88, 104, 123, 124syl113anc 1376 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → (𝑆 ↾ suc 𝑔) = (𝑝 ↾ suc 𝑔))
126125breq2d 5075 . . . . . . . . . . 11 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ((𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔) ↔ (𝑍 ↾ suc 𝑔) <s (𝑝 ↾ suc 𝑔)))
127111, 126mtbird 326 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ (𝑝𝐴 ∧ (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))))) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔))
128127rexlimdvaa 3290 . . . . . . . . 9 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (∃𝑝𝐴 (𝑔 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑔) = (𝑞 ↾ suc 𝑔))) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔)))
12987, 128sylbid 241 . . . . . . . 8 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑔 ∈ dom 𝑆 → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔)))
130129imp 407 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ¬ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔))
13169adantr 481 . . . . . . . . . . 11 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → 𝑆 No )
132 nodmord 33044 . . . . . . . . . . 11 (𝑆 No → Ord dom 𝑆)
133131, 132syl 17 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → Ord dom 𝑆)
134 simpr 485 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → 𝑔 ∈ dom 𝑆)
135 ordsucss 7521 . . . . . . . . . 10 (Ord dom 𝑆 → (𝑔 ∈ dom 𝑆 → suc 𝑔 ⊆ dom 𝑆))
136133, 134, 135sylc 65 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → suc 𝑔 ⊆ dom 𝑆)
137136resabs1d 5883 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) = (𝑍 ↾ suc 𝑔))
138136resabs1d 5883 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔) = (𝑆 ↾ suc 𝑔))
139137, 138breq12d 5076 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → (((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) <s ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔) ↔ (𝑍 ↾ suc 𝑔) <s (𝑆 ↾ suc 𝑔)))
140130, 139mtbird 326 . . . . . 6 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) ∧ 𝑔 ∈ dom 𝑆) → ¬ ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) <s ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔))
141140ralrimiva 3187 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ∀𝑔 ∈ dom 𝑆 ¬ ((𝑍 ↾ dom 𝑆) ↾ suc 𝑔) <s ((𝑆 ↾ dom 𝑆) ↾ suc 𝑔))
142 noresle 33084 . . . . 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 1371 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s (𝑆 ↾ dom 𝑆))
144 nofun 33040 . . . . . . 7 (𝑆 No → Fun 𝑆)
14569, 144syl 17 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → Fun 𝑆)
146 funrel 6369 . . . . . 6 (Fun 𝑆 → Rel 𝑆)
147 resdm 5896 . . . . . 6 (Rel 𝑆 → (𝑆 ↾ dom 𝑆) = 𝑆)
148145, 146, 1473syl 18 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → (𝑆 ↾ dom 𝑆) = 𝑆)
149148breq2d 5075 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ((𝑍 ↾ dom 𝑆) <s (𝑆 ↾ dom 𝑆) ↔ (𝑍 ↾ dom 𝑆) <s 𝑆))
150143, 149mtbid 325 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍)) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
15166, 150pm2.61ian 808 . 2 (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ∀𝑎𝐴 𝑎 <s 𝑍) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
152 simpll1 1206 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝐴 No )
153 simpll2 1207 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝐴 ∈ V)
154 simpr 485 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑎𝐴)
1553nosupbnd1 33098 . . . . . 6 ((𝐴 No 𝐴 ∈ V ∧ 𝑎𝐴) → (𝑎 ↾ dom 𝑆) <s 𝑆)
156152, 153, 154, 155syl3anc 1365 . . . . 5 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (𝑎 ↾ dom 𝑆) <s 𝑆)
157 simplr 765 . . . . 5 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → ¬ (𝑍 ↾ dom 𝑆) <s 𝑆)
158 simpl1 1185 . . . . . . . 8 (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → 𝐴 No )
159158sselda 3971 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑎 No )
160152, 153, 67syl2anc 584 . . . . . . . 8 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑆 No )
161160, 70syl 17 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → dom 𝑆 ∈ On)
162 noreson 33051 . . . . . . 7 ((𝑎 No ∧ dom 𝑆 ∈ On) → (𝑎 ↾ dom 𝑆) ∈ No )
163159, 161, 162syl2anc 584 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (𝑎 ↾ dom 𝑆) ∈ No )
164 simpll3 1208 . . . . . . 7 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑍 No )
165164, 161, 75syl2anc 584 . . . . . 6 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (𝑍 ↾ dom 𝑆) ∈ No )
166 sotr3 32886 . . . . . . 7 (( <s Or No ∧ ((𝑎 ↾ dom 𝑆) ∈ No 𝑆 No ∧ (𝑍 ↾ dom 𝑆) ∈ No )) → (((𝑎 ↾ dom 𝑆) <s 𝑆 ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆)))
16797, 166mpan 686 . . . . . 6 (((𝑎 ↾ dom 𝑆) ∈ No 𝑆 No ∧ (𝑍 ↾ dom 𝑆) ∈ No ) → (((𝑎 ↾ dom 𝑆) <s 𝑆 ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆)))
168163, 160, 165, 167syl3anc 1365 . . . . 5 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (((𝑎 ↾ dom 𝑆) <s 𝑆 ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆)))
169156, 157, 168mp2and 695 . . . 4 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → (𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆))
170 sltres 33053 . . . . 5 ((𝑎 No 𝑍 No ∧ dom 𝑆 ∈ On) → ((𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆) → 𝑎 <s 𝑍))
171159, 164, 161, 170syl3anc 1365 . . . 4 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → ((𝑎 ↾ dom 𝑆) <s (𝑍 ↾ dom 𝑆) → 𝑎 <s 𝑍))
172169, 171mpd 15 . . 3 ((((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) ∧ 𝑎𝐴) → 𝑎 <s 𝑍)
173172ralrimiva 3187 . 2 (((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) ∧ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆) → ∀𝑎𝐴 𝑎 <s 𝑍)
174151, 173impbida 797 1 ((𝐴 No 𝐴 ∈ V ∧ 𝑍 No ) → (∀𝑎𝐴 𝑎 <s 𝑍 ↔ ¬ (𝑍 ↾ dom 𝑆) <s 𝑆))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  {cab 2804  wral 3143  wrex 3144  ∃!wreu 3145  ∃*wrmo 3146  Vcvv 3500  cun 3938  cin 3939  wss 3940  ifcif 4470  {csn 4564  cop 4570   class class class wbr 5063  cmpt 5143   Or wor 5472  dom cdm 5554  cres 5556  Rel wrel 5559  Ord word 6188  Oncon0 6189  suc csuc 6191  cio 6310  Fun wfun 6346  cfv 6352  crio 7105  2oc2o 8087   No csur 33031   <s cslt 33032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-ord 6192  df-on 6193  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-riota 7106  df-1o 8093  df-2o 8094  df-no 33034  df-slt 33035  df-bday 33036
This theorem is referenced by:  noetalem3  33103
  Copyright terms: Public domain W3C validator