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

Theorem noinfbnd1lem1 33524
 Description: Lemma for noinfbnd1 33530. Establish a soft lower bound. (Contributed by Scott Fenton, 9-Aug-2024.)
Hypothesis
Ref Expression
noinfbnd1.1 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
noinfbnd1lem1 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇)
Distinct variable groups:   𝐵,𝑔,𝑢,𝑣,𝑥,𝑦   𝑣,𝑈   𝑥,𝑢,𝑦   𝑔,𝑉   𝑥,𝑣,𝑦
Allowed substitution hints:   𝑇(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑈(𝑥,𝑦,𝑢,𝑔)   𝑉(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem noinfbnd1lem1
Dummy variables 𝑝 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 noinfbnd1.1 . . . 4 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
21noinfno 33519 . . 3 ((𝐵 No 𝐵𝑉) → 𝑇 No )
323ad2ant2 1131 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝑇 No )
4 simp2l 1196 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝐵 No )
5 simp3 1135 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝑈𝐵)
64, 5sseldd 3895 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝑈 No )
7 nodmon 33451 . . . 4 (𝑇 No → dom 𝑇 ∈ On)
83, 7syl 17 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → dom 𝑇 ∈ On)
9 noreson 33461 . . 3 ((𝑈 No ∧ dom 𝑇 ∈ On) → (𝑈 ↾ dom 𝑇) ∈ No )
106, 8, 9syl2anc 587 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → (𝑈 ↾ dom 𝑇) ∈ No )
11 ssidd 3917 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → dom 𝑇 ⊆ dom 𝑇)
12 dmres 5850 . . . 4 dom (𝑈 ↾ dom 𝑇) = (dom 𝑇 ∩ dom 𝑈)
13 inss1 4135 . . . 4 (dom 𝑇 ∩ dom 𝑈) ⊆ dom 𝑇
1412, 13eqsstri 3928 . . 3 dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇
1514a1i 11 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇)
16 nodmord 33454 . . . . . . . 8 (𝑇 No → Ord dom 𝑇)
173, 16syl 17 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → Ord dom 𝑇)
18 ordsucss 7538 . . . . . . 7 (Ord dom 𝑇 → ( ∈ dom 𝑇 → suc ⊆ dom 𝑇))
1917, 18syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ( ∈ dom 𝑇 → suc ⊆ dom 𝑇))
2019imp 410 . . . . 5 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ ∈ dom 𝑇) → suc ⊆ dom 𝑇)
2120resabs1d 5859 . . . 4 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ ∈ dom 𝑇) → ((𝑈 ↾ dom 𝑇) ↾ suc ) = (𝑈 ↾ suc ))
221noinfdm 33520 . . . . . . . . 9 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = { ∣ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )))})
2322eleq2d 2837 . . . . . . . 8 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( ∈ dom 𝑇 ∈ { ∣ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )))}))
24 abid 2739 . . . . . . . . 9 ( ∈ { ∣ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )))} ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc ))))
25 breq2 5040 . . . . . . . . . . . . . 14 (𝑞 = 𝑣 → (𝑝 <s 𝑞𝑝 <s 𝑣))
2625notbid 321 . . . . . . . . . . . . 13 (𝑞 = 𝑣 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣))
27 reseq1 5822 . . . . . . . . . . . . . 14 (𝑞 = 𝑣 → (𝑞 ↾ suc ) = (𝑣 ↾ suc ))
2827eqeq2d 2769 . . . . . . . . . . . . 13 (𝑞 = 𝑣 → ((𝑝 ↾ suc ) = (𝑞 ↾ suc ) ↔ (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
2926, 28imbi12d 348 . . . . . . . . . . . 12 (𝑞 = 𝑣 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
3029cbvralvw 3361 . . . . . . . . . . 11 (∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )) ↔ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
3130anbi2i 625 . . . . . . . . . 10 (( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc ))) ↔ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
3231rexbii 3175 . . . . . . . . 9 (∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc ))) ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
3324, 32bitri 278 . . . . . . . 8 ( ∈ { ∣ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )))} ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
3423, 33bitrdi 290 . . . . . . 7 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( ∈ dom 𝑇 ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
35343ad2ant1 1130 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ( ∈ dom 𝑇 ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
36 simpl2l 1223 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝐵 No )
37 simprl 770 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑝𝐵)
3836, 37sseldd 3895 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑝 No )
396adantr 484 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑈 No )
40 sltso 33477 . . . . . . . . . . . 12 <s Or No
41 soasym 5477 . . . . . . . . . . . 12 (( <s Or No ∧ (𝑝 No 𝑈 No )) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
4240, 41mpan 689 . . . . . . . . . . 11 ((𝑝 No 𝑈 No ) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
4338, 39, 42syl2anc 587 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
44 nodmon 33451 . . . . . . . . . . . . . 14 (𝑝 No → dom 𝑝 ∈ On)
4538, 44syl 17 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → dom 𝑝 ∈ On)
46 simprrl 780 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∈ dom 𝑝)
47 onelon 6199 . . . . . . . . . . . . 13 ((dom 𝑝 ∈ On ∧ ∈ dom 𝑝) → ∈ On)
4845, 46, 47syl2anc 587 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∈ On)
49 sucelon 7537 . . . . . . . . . . . 12 ( ∈ On ↔ suc ∈ On)
5048, 49sylib 221 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → suc ∈ On)
51 sltres 33463 . . . . . . . . . . 11 ((𝑈 No 𝑝 No ∧ suc ∈ On) → ((𝑈 ↾ suc ) <s (𝑝 ↾ suc ) → 𝑈 <s 𝑝))
5239, 38, 50, 51syl3anc 1368 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ((𝑈 ↾ suc ) <s (𝑝 ↾ suc ) → 𝑈 <s 𝑝))
5343, 52nsyld 159 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → ¬ (𝑈 ↾ suc ) <s (𝑝 ↾ suc )))
54 noreson 33461 . . . . . . . . . . . . . 14 ((𝑈 No ∧ suc ∈ On) → (𝑈 ↾ suc ) ∈ No )
5539, 50, 54syl2anc 587 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑈 ↾ suc ) ∈ No )
56 sonr 5469 . . . . . . . . . . . . . 14 (( <s Or No ∧ (𝑈 ↾ suc ) ∈ No ) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
5740, 56mpan 689 . . . . . . . . . . . . 13 ((𝑈 ↾ suc ) ∈ No → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
5855, 57syl 17 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
5958adantr 484 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ ¬ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
60 breq2 5040 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑈 → (𝑝 <s 𝑣𝑝 <s 𝑈))
6160notbid 321 . . . . . . . . . . . . . . 15 (𝑣 = 𝑈 → (¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑈))
62 reseq1 5822 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑈 → (𝑣 ↾ suc ) = (𝑈 ↾ suc ))
6362eqeq2d 2769 . . . . . . . . . . . . . . 15 (𝑣 = 𝑈 → ((𝑝 ↾ suc ) = (𝑣 ↾ suc ) ↔ (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
6461, 63imbi12d 348 . . . . . . . . . . . . . 14 (𝑣 = 𝑈 → ((¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )) ↔ (¬ 𝑝 <s 𝑈 → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))))
65 simprrr 781 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
66 simpl3 1190 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑈𝐵)
6764, 65, 66rspcdva 3545 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (¬ 𝑝 <s 𝑈 → (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
6867imp 410 . . . . . . . . . . . 12 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ ¬ 𝑝 <s 𝑈) → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))
6968breq2d 5048 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ ¬ 𝑝 <s 𝑈) → ((𝑈 ↾ suc ) <s (𝑝 ↾ suc ) ↔ (𝑈 ↾ suc ) <s (𝑈 ↾ suc )))
7059, 69mtbird 328 . . . . . . . . . 10 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ ¬ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ) <s (𝑝 ↾ suc ))
7170ex 416 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (¬ 𝑝 <s 𝑈 → ¬ (𝑈 ↾ suc ) <s (𝑝 ↾ suc )))
7253, 71pm2.61d 182 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑈 ↾ suc ) <s (𝑝 ↾ suc ))
73 simpl1 1188 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
74 simpl2 1189 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝐵 No 𝐵𝑉))
751noinfres 33523 . . . . . . . . . 10 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑝𝐵 ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))) → (𝑇 ↾ suc ) = (𝑝 ↾ suc ))
7673, 74, 37, 46, 65, 75syl113anc 1379 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑇 ↾ suc ) = (𝑝 ↾ suc ))
7776breq2d 5048 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ((𝑈 ↾ suc ) <s (𝑇 ↾ suc ) ↔ (𝑈 ↾ suc ) <s (𝑝 ↾ suc )))
7872, 77mtbird 328 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑈 ↾ suc ) <s (𝑇 ↾ suc ))
7978rexlimdvaa 3209 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → (∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))) → ¬ (𝑈 ↾ suc ) <s (𝑇 ↾ suc )))
8035, 79sylbid 243 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ( ∈ dom 𝑇 → ¬ (𝑈 ↾ suc ) <s (𝑇 ↾ suc )))
8180imp 410 . . . 4 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ ∈ dom 𝑇) → ¬ (𝑈 ↾ suc ) <s (𝑇 ↾ suc ))
8221, 81eqnbrtrd 5054 . . 3 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ ∈ dom 𝑇) → ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ) <s (𝑇 ↾ suc ))
8382ralrimiva 3113 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ∀ ∈ dom 𝑇 ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ) <s (𝑇 ↾ suc ))
84 noresle 33498 . 2 (((𝑇 No ∧ (𝑈 ↾ dom 𝑇) ∈ No ) ∧ (dom 𝑇 ⊆ dom 𝑇 ∧ dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇 ∧ ∀ ∈ dom 𝑇 ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ) <s (𝑇 ↾ suc ))) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇)
853, 10, 11, 15, 83, 84syl23anc 1374 1 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {cab 2735  ∀wral 3070  ∃wrex 3071   ∪ cun 3858   ∩ cin 3859   ⊆ wss 3860  ifcif 4423  {csn 4525  ⟨cop 4531   class class class wbr 5036   ↦ cmpt 5116   Or wor 5446  dom cdm 5528   ↾ cres 5530  Ord word 6173  Oncon0 6174  suc csuc 6176  ℩cio 6297  ‘cfv 6340  ℩crio 7113  1oc1o 8111   No csur 33441
 Copyright terms: Public domain W3C validator