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

Theorem nosupbnd1lem1 33282
 Description: Lemma for nosupbnd1 33288. Establish a soft upper bound. (Contributed by Scott Fenton, 5-Dec-2021.)
Hypothesis
Ref Expression
nosupbnd1.1 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
nosupbnd1lem1 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ¬ 𝑆 <s (𝑈 ↾ dom 𝑆))
Distinct variable groups:   𝐴,𝑔,𝑢,𝑣,𝑥,𝑦   𝑣,𝑈   𝑥,𝑢,𝑦,𝑣
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑈(𝑥,𝑦,𝑢,𝑔)

Proof of Theorem nosupbnd1lem1
Dummy variables 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp2l 1196 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → 𝐴 No )
2 simp3 1135 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → 𝑈𝐴)
31, 2sseldd 3943 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → 𝑈 No )
4 nosupbnd1.1 . . . . . 6 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
54nosupno 33277 . . . . 5 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
653ad2ant2 1131 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → 𝑆 No )
7 nodmon 33231 . . . 4 (𝑆 No → dom 𝑆 ∈ On)
86, 7syl 17 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → dom 𝑆 ∈ On)
9 noreson 33241 . . 3 ((𝑈 No ∧ dom 𝑆 ∈ On) → (𝑈 ↾ dom 𝑆) ∈ No )
103, 8, 9syl2anc 587 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → (𝑈 ↾ dom 𝑆) ∈ No )
11 dmres 5853 . . . 4 dom (𝑈 ↾ dom 𝑆) = (dom 𝑆 ∩ dom 𝑈)
12 inss1 4179 . . . 4 (dom 𝑆 ∩ dom 𝑈) ⊆ dom 𝑆
1311, 12eqsstri 3976 . . 3 dom (𝑈 ↾ dom 𝑆) ⊆ dom 𝑆
1413a1i 11 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → dom (𝑈 ↾ dom 𝑆) ⊆ dom 𝑆)
15 ssidd 3965 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → dom 𝑆 ⊆ dom 𝑆)
16 iffalse 4448 . . . . . . . . . . . 12 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
174, 16syl5eq 2869 . . . . . . . . . . 11 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
1817dmeqd 5751 . . . . . . . . . 10 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
19 iotaex 6314 . . . . . . . . . . 11 (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) ∈ V
20 eqid 2822 . . . . . . . . . . 11 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
2119, 20dmmpti 6472 . . . . . . . . . 10 dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
2218, 21syl6eq 2873 . . . . . . . . 9 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
2322eleq2d 2899 . . . . . . . 8 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ( ∈ dom 𝑆 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
24 vex 3472 . . . . . . . . 9 ∈ V
25 eleq1w 2896 . . . . . . . . . . . 12 (𝑦 = → (𝑦 ∈ dom 𝑢 ∈ dom 𝑢))
26 suceq 6234 . . . . . . . . . . . . . . . 16 (𝑦 = → suc 𝑦 = suc )
2726reseq2d 5831 . . . . . . . . . . . . . . 15 (𝑦 = → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc ))
2826reseq2d 5831 . . . . . . . . . . . . . . 15 (𝑦 = → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc ))
2927, 28eqeq12d 2838 . . . . . . . . . . . . . 14 (𝑦 = → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc ) = (𝑣 ↾ suc )))
3029imbi2d 344 . . . . . . . . . . . . 13 (𝑦 = → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc ))))
3130ralbidv 3187 . . . . . . . . . . . 12 (𝑦 = → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc ))))
3225, 31anbi12d 633 . . . . . . . . . . 11 (𝑦 = → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ( ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc )))))
3332rexbidv 3283 . . . . . . . . . 10 (𝑦 = → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 ( ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc )))))
34 dmeq 5749 . . . . . . . . . . . . 13 (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
3534eleq2d 2899 . . . . . . . . . . . 12 (𝑢 = 𝑝 → ( ∈ dom 𝑢 ∈ dom 𝑝))
36 breq2 5046 . . . . . . . . . . . . . . 15 (𝑢 = 𝑝 → (𝑣 <s 𝑢𝑣 <s 𝑝))
3736notbid 321 . . . . . . . . . . . . . 14 (𝑢 = 𝑝 → (¬ 𝑣 <s 𝑢 ↔ ¬ 𝑣 <s 𝑝))
38 reseq1 5825 . . . . . . . . . . . . . . 15 (𝑢 = 𝑝 → (𝑢 ↾ suc ) = (𝑝 ↾ suc ))
3938eqeq1d 2824 . . . . . . . . . . . . . 14 (𝑢 = 𝑝 → ((𝑢 ↾ suc ) = (𝑣 ↾ suc ) ↔ (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
4037, 39imbi12d 348 . . . . . . . . . . . . 13 (𝑢 = 𝑝 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc )) ↔ (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
4140ralbidv 3187 . . . . . . . . . . . 12 (𝑢 = 𝑝 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc )) ↔ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
4235, 41anbi12d 633 . . . . . . . . . . 11 (𝑢 = 𝑝 → (( ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc ))) ↔ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
4342cbvrexvw 3425 . . . . . . . . . 10 (∃𝑢𝐴 ( ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc ))) ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
4433, 43syl6bb 290 . . . . . . . . 9 (𝑦 = → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
4524, 44elab 3642 . . . . . . . 8 ( ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
4623, 45syl6bb 290 . . . . . . 7 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ( ∈ dom 𝑆 ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
47463ad2ant1 1130 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ( ∈ dom 𝑆 ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
48 simpl1 1188 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
49 simpl2 1189 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝐴 No 𝐴 ∈ V))
50 simprl 770 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑝𝐴)
51 simprrl 780 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∈ dom 𝑝)
52 simprrr 781 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
534nosupres 33281 . . . . . . . . 9 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑝𝐴 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))) → (𝑆 ↾ suc ) = (𝑝 ↾ suc ))
5448, 49, 50, 51, 52, 53syl113anc 1379 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑆 ↾ suc ) = (𝑝 ↾ suc ))
55 simpl2l 1223 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝐴 No )
5655, 50sseldd 3943 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑝 No )
573adantr 484 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑈 No )
58 sltso 33255 . . . . . . . . . . . . . . 15 <s Or No
59 soasym 5481 . . . . . . . . . . . . . . 15 (( <s Or No ∧ (𝑝 No 𝑈 No )) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
6058, 59mpan 689 . . . . . . . . . . . . . 14 ((𝑝 No 𝑈 No ) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
6156, 57, 60syl2anc 587 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
62 simpl3 1190 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑈𝐴)
63 breq1 5045 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑈 → (𝑣 <s 𝑝𝑈 <s 𝑝))
6463notbid 321 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑈 → (¬ 𝑣 <s 𝑝 ↔ ¬ 𝑈 <s 𝑝))
65 reseq1 5825 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑈 → (𝑣 ↾ suc ) = (𝑈 ↾ suc ))
6665eqeq2d 2833 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑈 → ((𝑝 ↾ suc ) = (𝑣 ↾ suc ) ↔ (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
6764, 66imbi12d 348 . . . . . . . . . . . . . . 15 (𝑣 = 𝑈 → ((¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )) ↔ (¬ 𝑈 <s 𝑝 → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))))
6867rspcv 3593 . . . . . . . . . . . . . 14 (𝑈𝐴 → (∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )) → (¬ 𝑈 <s 𝑝 → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))))
6962, 52, 68sylc 65 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (¬ 𝑈 <s 𝑝 → (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
7061, 69syld 47 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
7170imp 410 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ 𝑝 <s 𝑈) → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))
72 nodmon 33231 . . . . . . . . . . . . . . . . 17 (𝑝 No → dom 𝑝 ∈ On)
7356, 72syl 17 . . . . . . . . . . . . . . . 16 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → dom 𝑝 ∈ On)
74 onelon 6194 . . . . . . . . . . . . . . . 16 ((dom 𝑝 ∈ On ∧ ∈ dom 𝑝) → ∈ On)
7573, 51, 74syl2anc 587 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∈ On)
76 sucelon 7517 . . . . . . . . . . . . . . 15 ( ∈ On ↔ suc ∈ On)
7775, 76sylib 221 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → suc ∈ On)
78 noreson 33241 . . . . . . . . . . . . . 14 ((𝑈 No ∧ suc ∈ On) → (𝑈 ↾ suc ) ∈ No )
7957, 77, 78syl2anc 587 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑈 ↾ suc ) ∈ No )
80 sonr 5473 . . . . . . . . . . . . . 14 (( <s Or No ∧ (𝑈 ↾ suc ) ∈ No ) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
8158, 80mpan 689 . . . . . . . . . . . . 13 ((𝑈 ↾ suc ) ∈ No → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
8279, 81syl 17 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
8382adantr 484 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
8471, 83eqnbrtrd 5060 . . . . . . . . . 10 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ 𝑝 <s 𝑈) → ¬ (𝑝 ↾ suc ) <s (𝑈 ↾ suc ))
8584ex 416 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → ¬ (𝑝 ↾ suc ) <s (𝑈 ↾ suc )))
86 sltres 33243 . . . . . . . . . . 11 ((𝑝 No 𝑈 No ∧ suc ∈ On) → ((𝑝 ↾ suc ) <s (𝑈 ↾ suc ) → 𝑝 <s 𝑈))
8756, 57, 77, 86syl3anc 1368 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ((𝑝 ↾ suc ) <s (𝑈 ↾ suc ) → 𝑝 <s 𝑈))
8887con3d 155 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (¬ 𝑝 <s 𝑈 → ¬ (𝑝 ↾ suc ) <s (𝑈 ↾ suc )))
8985, 88pm2.61d 182 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑝 ↾ suc ) <s (𝑈 ↾ suc ))
9054, 89eqnbrtrd 5060 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑆 ↾ suc ) <s (𝑈 ↾ suc ))
9190rexlimdvaa 3271 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → (∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))) → ¬ (𝑆 ↾ suc ) <s (𝑈 ↾ suc )))
9247, 91sylbid 243 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ( ∈ dom 𝑆 → ¬ (𝑆 ↾ suc ) <s (𝑈 ↾ suc )))
9392imp 410 . . . 4 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → ¬ (𝑆 ↾ suc ) <s (𝑈 ↾ suc ))
94 nodmord 33234 . . . . . . . 8 (𝑆 No → Ord dom 𝑆)
95 ordsucss 7518 . . . . . . . 8 (Ord dom 𝑆 → ( ∈ dom 𝑆 → suc ⊆ dom 𝑆))
966, 94, 953syl 18 . . . . . . 7 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ( ∈ dom 𝑆 → suc ⊆ dom 𝑆))
9796imp 410 . . . . . 6 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → suc ⊆ dom 𝑆)
9897resabs1d 5862 . . . . 5 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → ((𝑈 ↾ dom 𝑆) ↾ suc ) = (𝑈 ↾ suc ))
9998breq2d 5054 . . . 4 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → ((𝑆 ↾ suc ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ) ↔ (𝑆 ↾ suc ) <s (𝑈 ↾ suc )))
10093, 99mtbird 328 . . 3 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → ¬ (𝑆 ↾ suc ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ))
101100ralrimiva 3174 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ∀ ∈ dom 𝑆 ¬ (𝑆 ↾ suc ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ))
102 noresle 33274 . 2 ((((𝑈 ↾ dom 𝑆) ∈ No 𝑆 No ) ∧ (dom (𝑈 ↾ dom 𝑆) ⊆ dom 𝑆 ∧ dom 𝑆 ⊆ dom 𝑆 ∧ ∀ ∈ dom 𝑆 ¬ (𝑆 ↾ suc ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ))) → ¬ 𝑆 <s (𝑈 ↾ dom 𝑆))
10310, 6, 14, 15, 101, 102syl23anc 1374 1 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ¬ 𝑆 <s (𝑈 ↾ dom 𝑆))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2114  {cab 2800  ∀wral 3130  ∃wrex 3131  Vcvv 3469   ∪ cun 3906   ∩ cin 3907   ⊆ wss 3908  ifcif 4439  {csn 4539  ⟨cop 4545   class class class wbr 5042   ↦ cmpt 5122   Or wor 5450  dom cdm 5532   ↾ cres 5534  Ord word 6168  Oncon0 6169  suc csuc 6171  ℩cio 6291  ‘cfv 6334  ℩crio 7097  2oc2o 8083   No csur 33221
 Copyright terms: Public domain W3C validator