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

Theorem nosupbnd1lem1 27754
Description: Lemma for nosupbnd1 27760. 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 1199 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → 𝐴 No )
2 simp3 1138 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → 𝑈𝐴)
31, 2sseldd 3983 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → 𝑈 No )
4 nosupbnd1.1 . . . . . 6 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
54nosupno 27749 . . . . 5 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
653ad2ant2 1134 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → 𝑆 No )
7 nodmon 27696 . . . 4 (𝑆 No → dom 𝑆 ∈ On)
86, 7syl 17 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → dom 𝑆 ∈ On)
9 noreson 27706 . . 3 ((𝑈 No ∧ dom 𝑆 ∈ On) → (𝑈 ↾ dom 𝑆) ∈ No )
103, 8, 9syl2anc 584 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → (𝑈 ↾ dom 𝑆) ∈ No )
11 dmres 6029 . . . 4 dom (𝑈 ↾ dom 𝑆) = (dom 𝑆 ∩ dom 𝑈)
12 inss1 4236 . . . 4 (dom 𝑆 ∩ dom 𝑈) ⊆ dom 𝑆
1311, 12eqsstri 4029 . . 3 dom (𝑈 ↾ dom 𝑆) ⊆ dom 𝑆
1413a1i 11 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → dom (𝑈 ↾ dom 𝑆) ⊆ dom 𝑆)
15 ssidd 4006 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → dom 𝑆 ⊆ dom 𝑆)
16 iffalse 4533 . . . . . . . . . . . 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, 16eqtrid 2788 . . . . . . . . . . 11 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
1817dmeqd 5915 . . . . . . . . . 10 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
19 iotaex 6533 . . . . . . . . . . 11 (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) ∈ V
20 eqid 2736 . . . . . . . . . . 11 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
2119, 20dmmpti 6711 . . . . . . . . . 10 dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
2218, 21eqtrdi 2792 . . . . . . . . 9 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
2322eleq2d 2826 . . . . . . . 8 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ( ∈ dom 𝑆 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
24 vex 3483 . . . . . . . . 9 ∈ V
25 eleq1w 2823 . . . . . . . . . . . 12 (𝑦 = → (𝑦 ∈ dom 𝑢 ∈ dom 𝑢))
26 suceq 6449 . . . . . . . . . . . . . . . 16 (𝑦 = → suc 𝑦 = suc )
2726reseq2d 5996 . . . . . . . . . . . . . . 15 (𝑦 = → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc ))
2826reseq2d 5996 . . . . . . . . . . . . . . 15 (𝑦 = → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc ))
2927, 28eqeq12d 2752 . . . . . . . . . . . . . 14 (𝑦 = → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc ) = (𝑣 ↾ suc )))
3029imbi2d 340 . . . . . . . . . . . . 13 (𝑦 = → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc ))))
3130ralbidv 3177 . . . . . . . . . . . 12 (𝑦 = → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc ))))
3225, 31anbi12d 632 . . . . . . . . . . 11 (𝑦 = → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ( ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc )))))
3332rexbidv 3178 . . . . . . . . . 10 (𝑦 = → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 ( ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc )))))
34 dmeq 5913 . . . . . . . . . . . . 13 (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
3534eleq2d 2826 . . . . . . . . . . . 12 (𝑢 = 𝑝 → ( ∈ dom 𝑢 ∈ dom 𝑝))
36 breq2 5146 . . . . . . . . . . . . . . 15 (𝑢 = 𝑝 → (𝑣 <s 𝑢𝑣 <s 𝑝))
3736notbid 318 . . . . . . . . . . . . . 14 (𝑢 = 𝑝 → (¬ 𝑣 <s 𝑢 ↔ ¬ 𝑣 <s 𝑝))
38 reseq1 5990 . . . . . . . . . . . . . . 15 (𝑢 = 𝑝 → (𝑢 ↾ suc ) = (𝑝 ↾ suc ))
3938eqeq1d 2738 . . . . . . . . . . . . . 14 (𝑢 = 𝑝 → ((𝑢 ↾ suc ) = (𝑣 ↾ suc ) ↔ (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
4037, 39imbi12d 344 . . . . . . . . . . . . 13 (𝑢 = 𝑝 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc )) ↔ (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
4140ralbidv 3177 . . . . . . . . . . . 12 (𝑢 = 𝑝 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc )) ↔ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
4235, 41anbi12d 632 . . . . . . . . . . 11 (𝑢 = 𝑝 → (( ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc ))) ↔ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
4342cbvrexvw 3237 . . . . . . . . . 10 (∃𝑢𝐴 ( ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc ))) ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
4433, 43bitrdi 287 . . . . . . . . 9 (𝑦 = → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
4524, 44elab 3678 . . . . . . . 8 ( ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
4623, 45bitrdi 287 . . . . . . 7 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ( ∈ dom 𝑆 ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
47463ad2ant1 1133 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ( ∈ dom 𝑆 ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
48 simpl1 1191 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
49 simpl2 1192 . . . . . . . . 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 27753 . . . . . . . . 9 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑝𝐴 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))) → (𝑆 ↾ suc ) = (𝑝 ↾ suc ))
5448, 49, 50, 51, 52, 53syl113anc 1383 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑆 ↾ suc ) = (𝑝 ↾ suc ))
55 simpl2l 1226 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝐴 No )
5655, 50sseldd 3983 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑝 No )
573adantr 480 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑈 No )
58 sltso 27722 . . . . . . . . . . . . . . 15 <s Or No
59 soasym 5624 . . . . . . . . . . . . . . 15 (( <s Or No ∧ (𝑝 No 𝑈 No )) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
6058, 59mpan 690 . . . . . . . . . . . . . 14 ((𝑝 No 𝑈 No ) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
6156, 57, 60syl2anc 584 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
62 simpl3 1193 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑈𝐴)
63 breq1 5145 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑈 → (𝑣 <s 𝑝𝑈 <s 𝑝))
6463notbid 318 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑈 → (¬ 𝑣 <s 𝑝 ↔ ¬ 𝑈 <s 𝑝))
65 reseq1 5990 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑈 → (𝑣 ↾ suc ) = (𝑈 ↾ suc ))
6665eqeq2d 2747 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑈 → ((𝑝 ↾ suc ) = (𝑣 ↾ suc ) ↔ (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
6764, 66imbi12d 344 . . . . . . . . . . . . . . 15 (𝑣 = 𝑈 → ((¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )) ↔ (¬ 𝑈 <s 𝑝 → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))))
6867rspcv 3617 . . . . . . . . . . . . . 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 406 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ 𝑝 <s 𝑈) → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))
72 nodmon 27696 . . . . . . . . . . . . . . . . 17 (𝑝 No → dom 𝑝 ∈ On)
7356, 72syl 17 . . . . . . . . . . . . . . . 16 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → dom 𝑝 ∈ On)
74 onelon 6408 . . . . . . . . . . . . . . . 16 ((dom 𝑝 ∈ On ∧ ∈ dom 𝑝) → ∈ On)
7573, 51, 74syl2anc 584 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∈ On)
76 onsucb 7838 . . . . . . . . . . . . . . 15 ( ∈ On ↔ suc ∈ On)
7775, 76sylib 218 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → suc ∈ On)
78 noreson 27706 . . . . . . . . . . . . . 14 ((𝑈 No ∧ suc ∈ On) → (𝑈 ↾ suc ) ∈ No )
7957, 77, 78syl2anc 584 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑈 ↾ suc ) ∈ No )
80 sonr 5615 . . . . . . . . . . . . . 14 (( <s Or No ∧ (𝑈 ↾ suc ) ∈ No ) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
8158, 80mpan 690 . . . . . . . . . . . . 13 ((𝑈 ↾ suc ) ∈ No → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
8279, 81syl 17 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
8382adantr 480 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
8471, 83eqnbrtrd 5160 . . . . . . . . . 10 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ 𝑝 <s 𝑈) → ¬ (𝑝 ↾ suc ) <s (𝑈 ↾ suc ))
8584ex 412 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → ¬ (𝑝 ↾ suc ) <s (𝑈 ↾ suc )))
86 sltres 27708 . . . . . . . . . . 11 ((𝑝 No 𝑈 No ∧ suc ∈ On) → ((𝑝 ↾ suc ) <s (𝑈 ↾ suc ) → 𝑝 <s 𝑈))
8756, 57, 77, 86syl3anc 1372 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ((𝑝 ↾ suc ) <s (𝑈 ↾ suc ) → 𝑝 <s 𝑈))
8887con3d 152 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (¬ 𝑝 <s 𝑈 → ¬ (𝑝 ↾ suc ) <s (𝑈 ↾ suc )))
8985, 88pm2.61d 179 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑝 ↾ suc ) <s (𝑈 ↾ suc ))
9054, 89eqnbrtrd 5160 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑆 ↾ suc ) <s (𝑈 ↾ suc ))
9190rexlimdvaa 3155 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → (∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))) → ¬ (𝑆 ↾ suc ) <s (𝑈 ↾ suc )))
9247, 91sylbid 240 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ( ∈ dom 𝑆 → ¬ (𝑆 ↾ suc ) <s (𝑈 ↾ suc )))
9392imp 406 . . . 4 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → ¬ (𝑆 ↾ suc ) <s (𝑈 ↾ suc ))
94 nodmord 27699 . . . . . . . 8 (𝑆 No → Ord dom 𝑆)
95 ordsucss 7839 . . . . . . . 8 (Ord dom 𝑆 → ( ∈ dom 𝑆 → suc ⊆ dom 𝑆))
966, 94, 953syl 18 . . . . . . 7 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ( ∈ dom 𝑆 → suc ⊆ dom 𝑆))
9796imp 406 . . . . . 6 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → suc ⊆ dom 𝑆)
9897resabs1d 6025 . . . . 5 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → ((𝑈 ↾ dom 𝑆) ↾ suc ) = (𝑈 ↾ suc ))
9998breq2d 5154 . . . 4 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → ((𝑆 ↾ suc ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ) ↔ (𝑆 ↾ suc ) <s (𝑈 ↾ suc )))
10093, 99mtbird 325 . . 3 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → ¬ (𝑆 ↾ suc ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ))
101100ralrimiva 3145 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ∀ ∈ dom 𝑆 ¬ (𝑆 ↾ suc ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ))
102 noresle 27743 . 2 ((((𝑈 ↾ dom 𝑆) ∈ No 𝑆 No ) ∧ (dom (𝑈 ↾ dom 𝑆) ⊆ dom 𝑆 ∧ dom 𝑆 ⊆ dom 𝑆 ∧ ∀ ∈ dom 𝑆 ¬ (𝑆 ↾ suc ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ))) → ¬ 𝑆 <s (𝑈 ↾ dom 𝑆))
10310, 6, 14, 15, 101, 102syl23anc 1378 1 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ¬ 𝑆 <s (𝑈 ↾ dom 𝑆))
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  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  Ord word 6382  Oncon0 6383  suc csuc 6385  cio 6511  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-fo 6566  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:  nosupbnd1lem2  27755  nosupbnd1lem6  27759
  Copyright terms: Public domain W3C validator