Users' Mathboxes 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   <s cslt 32122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2142  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741  ax-rep 4924  ax-sep 4934  ax-nul 4942  ax-pow 4993  ax-pr 5056  ax-un 7116
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-eu 2612  df-mo 2613  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ne 2934  df-ral 3056  df-rex 3057  df-reu 3058  df-rmo 3059  df-rab 3060  df-v 3343  df-sbc 3578  df-csb 3676  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-pss 3732  df-nul 4060  df-if 4232  df-pw 4305  df-sn 4323  df-pr 4325  df-tp 4327  df-op 4329  df-uni 4590  df-int 4629  df-iun 4675  df-br 4806  df-opab 4866  df-mpt 4883  df-tr 4906  df-id 5175  df-eprel 5180  df-po 5188  df-so 5189  df-fr 5226  df-we 5228  df-xp 5273  df-rel 5274  df-cnv 5275  df-co 5276  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280  df-ord 5888  df-on 5889  df-suc 5891  df-iota 6013  df-fun 6052  df-fn 6053  df-f 6054  df-f1 6055  df-fo 6056  df-f1o 6057  df-fv 6058  df-riota 6776  df-1o 7731  df-2o 7732  df-no 32124  df-slt 32125  df-bday 32126
This theorem is referenced by:  nosupbnd1lem2  32183  nosupbnd1lem6  32187
  Copyright terms: Public domain W3C validator