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

Theorem nosupbnd1lem1 32182
 Description: Lemma for nosupbnd1 32188. Establish a soft upper bound. (Contributed by Scott Fenton, 5-Dec-2021.)
Hypothesis
Ref Expression
nosupbnd1.1 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ 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 1242 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → 𝐴 No )
2 simp3 1133 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → 𝑈𝐴)
31, 2sseldd 3746 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → 𝑈 No )
4 nosupbnd1.1 . . . . . 6 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
54nosupno 32177 . . . . 5 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
653ad2ant2 1129 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → 𝑆 No )
7 nodmon 32131 . . . 4 (𝑆 No → dom 𝑆 ∈ On)
86, 7syl 17 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → dom 𝑆 ∈ On)
9 noreson 32141 . . 3 ((𝑈 No ∧ dom 𝑆 ∈ On) → (𝑈 ↾ dom 𝑆) ∈ No )
103, 8, 9syl2anc 696 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → (𝑈 ↾ dom 𝑆) ∈ No )
11 dmres 5578 . . . 4 dom (𝑈 ↾ dom 𝑆) = (dom 𝑆 ∩ dom 𝑈)
12 inss1 3977 . . . 4 (dom 𝑆 ∩ dom 𝑈) ⊆ dom 𝑆
1311, 12eqsstri 3777 . . 3 dom (𝑈 ↾ dom 𝑆) ⊆ dom 𝑆
1413a1i 11 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → dom (𝑈 ↾ dom 𝑆) ⊆ dom 𝑆)
15 ssid 3766 . . 3 dom 𝑆 ⊆ dom 𝑆
1615a1i 11 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → dom 𝑆 ⊆ dom 𝑆)
17 iffalse 4240 . . . . . . . . . . . 12 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
184, 17syl5eq 2807 . . . . . . . . . . 11 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
1918dmeqd 5482 . . . . . . . . . 10 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
20 iotaex 6030 . . . . . . . . . . 11 (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) ∈ V
21 eqid 2761 . . . . . . . . . . 11 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
2220, 21dmmpti 6185 . . . . . . . . . 10 dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
2319, 22syl6eq 2811 . . . . . . . . 9 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
2423eleq2d 2826 . . . . . . . 8 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ( ∈ dom 𝑆 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
25 vex 3344 . . . . . . . . 9 ∈ V
26 eleq1w 2823 . . . . . . . . . . . 12 (𝑦 = → (𝑦 ∈ dom 𝑢 ∈ dom 𝑢))
27 suceq 5952 . . . . . . . . . . . . . . . 16 (𝑦 = → suc 𝑦 = suc )
2827reseq2d 5552 . . . . . . . . . . . . . . 15 (𝑦 = → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc ))
2927reseq2d 5552 . . . . . . . . . . . . . . 15 (𝑦 = → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc ))
3028, 29eqeq12d 2776 . . . . . . . . . . . . . 14 (𝑦 = → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc ) = (𝑣 ↾ suc )))
3130imbi2d 329 . . . . . . . . . . . . 13 (𝑦 = → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc ))))
3231ralbidv 3125 . . . . . . . . . . . 12 (𝑦 = → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc ))))
3326, 32anbi12d 749 . . . . . . . . . . 11 (𝑦 = → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ( ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc )))))
3433rexbidv 3191 . . . . . . . . . 10 (𝑦 = → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 ( ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc )))))
35 dmeq 5480 . . . . . . . . . . . . 13 (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
3635eleq2d 2826 . . . . . . . . . . . 12 (𝑢 = 𝑝 → ( ∈ dom 𝑢 ∈ dom 𝑝))
37 breq2 4809 . . . . . . . . . . . . . . 15 (𝑢 = 𝑝 → (𝑣 <s 𝑢𝑣 <s 𝑝))
3837notbid 307 . . . . . . . . . . . . . 14 (𝑢 = 𝑝 → (¬ 𝑣 <s 𝑢 ↔ ¬ 𝑣 <s 𝑝))
39 reseq1 5546 . . . . . . . . . . . . . . 15 (𝑢 = 𝑝 → (𝑢 ↾ suc ) = (𝑝 ↾ suc ))
4039eqeq1d 2763 . . . . . . . . . . . . . 14 (𝑢 = 𝑝 → ((𝑢 ↾ suc ) = (𝑣 ↾ suc ) ↔ (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
4138, 40imbi12d 333 . . . . . . . . . . . . 13 (𝑢 = 𝑝 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc )) ↔ (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
4241ralbidv 3125 . . . . . . . . . . . 12 (𝑢 = 𝑝 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc )) ↔ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
4336, 42anbi12d 749 . . . . . . . . . . 11 (𝑢 = 𝑝 → (( ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc ))) ↔ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
4443cbvrexv 3312 . . . . . . . . . 10 (∃𝑢𝐴 ( ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc ) = (𝑣 ↾ suc ))) ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
4534, 44syl6bb 276 . . . . . . . . 9 (𝑦 = → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
4625, 45elab 3491 . . . . . . . 8 ( ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
4724, 46syl6bb 276 . . . . . . 7 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ( ∈ dom 𝑆 ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
48473ad2ant1 1128 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ( ∈ dom 𝑆 ↔ ∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
49 simpl1 1228 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
50 simpl2 1230 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝐴 No 𝐴 ∈ V))
51 simprl 811 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑝𝐴)
52 simprrl 823 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∈ dom 𝑝)
53 simprrr 824 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
544nosupres 32181 . . . . . . . . 9 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑝𝐴 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))) → (𝑆 ↾ suc ) = (𝑝 ↾ suc ))
5549, 50, 51, 52, 53, 54syl113anc 1489 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑆 ↾ suc ) = (𝑝 ↾ suc ))
56 simpl2l 1283 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝐴 No )
5756, 51sseldd 3746 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑝 No )
583adantr 472 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑈 No )
59 sltso 32155 . . . . . . . . . . . . . . 15 <s Or No
60 soasym 31986 . . . . . . . . . . . . . . 15 (( <s Or No ∧ (𝑝 No 𝑈 No )) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
6159, 60mpan 708 . . . . . . . . . . . . . 14 ((𝑝 No 𝑈 No ) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
6257, 58, 61syl2anc 696 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
63 simpl3 1232 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑈𝐴)
64 breq1 4808 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑈 → (𝑣 <s 𝑝𝑈 <s 𝑝))
6564notbid 307 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑈 → (¬ 𝑣 <s 𝑝 ↔ ¬ 𝑈 <s 𝑝))
66 reseq1 5546 . . . . . . . . . . . . . . . . 17 (𝑣 = 𝑈 → (𝑣 ↾ suc ) = (𝑈 ↾ suc ))
6766eqeq2d 2771 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑈 → ((𝑝 ↾ suc ) = (𝑣 ↾ suc ) ↔ (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
6865, 67imbi12d 333 . . . . . . . . . . . . . . 15 (𝑣 = 𝑈 → ((¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )) ↔ (¬ 𝑈 <s 𝑝 → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))))
6968rspcv 3446 . . . . . . . . . . . . . 14 (𝑈𝐴 → (∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )) → (¬ 𝑈 <s 𝑝 → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))))
7063, 53, 69sylc 65 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (¬ 𝑈 <s 𝑝 → (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
7162, 70syld 47 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
7271imp 444 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ 𝑝 <s 𝑈) → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))
73 nodmon 32131 . . . . . . . . . . . . . . . . 17 (𝑝 No → dom 𝑝 ∈ On)
7457, 73syl 17 . . . . . . . . . . . . . . . 16 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → dom 𝑝 ∈ On)
75 onelon 5910 . . . . . . . . . . . . . . . 16 ((dom 𝑝 ∈ On ∧ ∈ dom 𝑝) → ∈ On)
7674, 52, 75syl2anc 696 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∈ On)
77 sucelon 7184 . . . . . . . . . . . . . . 15 ( ∈ On ↔ suc ∈ On)
7876, 77sylib 208 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → suc ∈ On)
79 noreson 32141 . . . . . . . . . . . . . 14 ((𝑈 No ∧ suc ∈ On) → (𝑈 ↾ suc ) ∈ No )
8058, 78, 79syl2anc 696 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑈 ↾ suc ) ∈ No )
81 sonr 5209 . . . . . . . . . . . . . 14 (( <s Or No ∧ (𝑈 ↾ suc ) ∈ No ) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
8259, 81mpan 708 . . . . . . . . . . . . 13 ((𝑈 ↾ suc ) ∈ No → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
8380, 82syl 17 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
8483adantr 472 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
8572, 84eqnbrtrd 4823 . . . . . . . . . 10 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ 𝑝 <s 𝑈) → ¬ (𝑝 ↾ suc ) <s (𝑈 ↾ suc ))
8685ex 449 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → ¬ (𝑝 ↾ suc ) <s (𝑈 ↾ suc )))
87 sltres 32143 . . . . . . . . . . 11 ((𝑝 No 𝑈 No ∧ suc ∈ On) → ((𝑝 ↾ suc ) <s (𝑈 ↾ suc ) → 𝑝 <s 𝑈))
8857, 58, 78, 87syl3anc 1477 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ((𝑝 ↾ suc ) <s (𝑈 ↾ suc ) → 𝑝 <s 𝑈))
8988con3d 148 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (¬ 𝑝 <s 𝑈 → ¬ (𝑝 ↾ suc ) <s (𝑈 ↾ suc )))
9086, 89pm2.61d 170 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑝 ↾ suc ) <s (𝑈 ↾ suc ))
9155, 90eqnbrtrd 4823 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ (𝑝𝐴 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑆 ↾ suc ) <s (𝑈 ↾ suc ))
9291rexlimdvaa 3171 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → (∃𝑝𝐴 ( ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))) → ¬ (𝑆 ↾ suc ) <s (𝑈 ↾ suc )))
9348, 92sylbid 230 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ( ∈ dom 𝑆 → ¬ (𝑆 ↾ suc ) <s (𝑈 ↾ suc )))
9493imp 444 . . . 4 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → ¬ (𝑆 ↾ suc ) <s (𝑈 ↾ suc ))
95 nodmord 32134 . . . . . . . 8 (𝑆 No → Ord dom 𝑆)
96 ordsucss 7185 . . . . . . . 8 (Ord dom 𝑆 → ( ∈ dom 𝑆 → suc ⊆ dom 𝑆))
976, 95, 963syl 18 . . . . . . 7 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ( ∈ dom 𝑆 → suc ⊆ dom 𝑆))
9897imp 444 . . . . . 6 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → suc ⊆ dom 𝑆)
9998resabs1d 5587 . . . . 5 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → ((𝑈 ↾ dom 𝑆) ↾ suc ) = (𝑈 ↾ suc ))
10099breq2d 4817 . . . 4 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → ((𝑆 ↾ suc ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ) ↔ (𝑆 ↾ suc ) <s (𝑈 ↾ suc )))
10194, 100mtbird 314 . . 3 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) ∧ ∈ dom 𝑆) → ¬ (𝑆 ↾ suc ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ))
102101ralrimiva 3105 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ∀ ∈ dom 𝑆 ¬ (𝑆 ↾ suc ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ))
103 noresle 32174 . 2 ((((𝑈 ↾ dom 𝑆) ∈ No 𝑆 No ) ∧ (dom (𝑈 ↾ dom 𝑆) ⊆ dom 𝑆 ∧ dom 𝑆 ⊆ dom 𝑆 ∧ ∀ ∈ dom 𝑆 ¬ (𝑆 ↾ suc ) <s ((𝑈 ↾ dom 𝑆) ↾ suc ))) → ¬ 𝑆 <s (𝑈 ↾ dom 𝑆))
10410, 6, 14, 16, 102, 103syl23anc 1484 1 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ 𝑈𝐴) → ¬ 𝑆 <s (𝑈 ↾ dom 𝑆))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2140  {cab 2747  ∀wral 3051  ∃wrex 3052  Vcvv 3341   ∪ cun 3714   ∩ cin 3715   ⊆ wss 3716  ifcif 4231  {csn 4322  ⟨cop 4328   class class class wbr 4805   ↦ cmpt 4882   Or wor 5187  dom cdm 5267   ↾ cres 5269  Ord word 5884  Oncon0 5885  suc csuc 5887  ℩cio 6011  ‘cfv 6050  ℩crio 6775  2𝑜c2o 7725   No csur 32121
 Copyright terms: Public domain W3C validator