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

Theorem noinfbnd1lem1 27023
Description: Lemma for noinfbnd1 27029. 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 27018 . . 3 ((𝐵 No 𝐵𝑉) → 𝑇 No )
323ad2ant2 1134 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝑇 No )
4 simp2l 1199 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝐵 No )
5 simp3 1138 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝑈𝐵)
64, 5sseldd 3943 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝑈 No )
7 nodmon 26950 . . . 4 (𝑇 No → dom 𝑇 ∈ On)
83, 7syl 17 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → dom 𝑇 ∈ On)
9 noreson 26960 . . 3 ((𝑈 No ∧ dom 𝑇 ∈ On) → (𝑈 ↾ dom 𝑇) ∈ No )
106, 8, 9syl2anc 584 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → (𝑈 ↾ dom 𝑇) ∈ No )
11 ssidd 3965 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → dom 𝑇 ⊆ dom 𝑇)
12 dmres 5957 . . . 4 dom (𝑈 ↾ dom 𝑇) = (dom 𝑇 ∩ dom 𝑈)
13 inss1 4186 . . . 4 (dom 𝑇 ∩ dom 𝑈) ⊆ dom 𝑇
1412, 13eqsstri 3976 . . 3 dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇
1514a1i 11 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇)
16 nodmord 26953 . . . . . . . 8 (𝑇 No → Ord dom 𝑇)
173, 16syl 17 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → Ord dom 𝑇)
18 ordsucss 7745 . . . . . . 7 (Ord dom 𝑇 → ( ∈ dom 𝑇 → suc ⊆ dom 𝑇))
1917, 18syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ( ∈ dom 𝑇 → suc ⊆ dom 𝑇))
2019imp 407 . . . . 5 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ ∈ dom 𝑇) → suc ⊆ dom 𝑇)
2120resabs1d 5966 . . . 4 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ ∈ dom 𝑇) → ((𝑈 ↾ dom 𝑇) ↾ suc ) = (𝑈 ↾ suc ))
221noinfdm 27019 . . . . . . . . 9 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = { ∣ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )))})
2322eleq2d 2823 . . . . . . . 8 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( ∈ dom 𝑇 ∈ { ∣ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )))}))
24 abid 2718 . . . . . . . . 9 ( ∈ { ∣ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )))} ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc ))))
25 breq2 5107 . . . . . . . . . . . . . 14 (𝑞 = 𝑣 → (𝑝 <s 𝑞𝑝 <s 𝑣))
2625notbid 317 . . . . . . . . . . . . 13 (𝑞 = 𝑣 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣))
27 reseq1 5929 . . . . . . . . . . . . . 14 (𝑞 = 𝑣 → (𝑞 ↾ suc ) = (𝑣 ↾ suc ))
2827eqeq2d 2748 . . . . . . . . . . . . 13 (𝑞 = 𝑣 → ((𝑝 ↾ suc ) = (𝑞 ↾ suc ) ↔ (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
2926, 28imbi12d 344 . . . . . . . . . . . 12 (𝑞 = 𝑣 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
3029cbvralvw 3223 . . . . . . . . . . 11 (∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )) ↔ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
3130anbi2i 623 . . . . . . . . . 10 (( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc ))) ↔ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
3231rexbii 3095 . . . . . . . . 9 (∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc ))) ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
3324, 32bitri 274 . . . . . . . 8 ( ∈ { ∣ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )))} ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
3423, 33bitrdi 286 . . . . . . 7 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( ∈ dom 𝑇 ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
35343ad2ant1 1133 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ( ∈ dom 𝑇 ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
36 simpl2l 1226 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝐵 No )
37 simprl 769 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑝𝐵)
3836, 37sseldd 3943 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑝 No )
396adantr 481 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑈 No )
40 sltso 26976 . . . . . . . . . . . 12 <s Or No
41 soasym 5574 . . . . . . . . . . . 12 (( <s Or No ∧ (𝑝 No 𝑈 No )) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
4240, 41mpan 688 . . . . . . . . . . 11 ((𝑝 No 𝑈 No ) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
4338, 39, 42syl2anc 584 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
44 nodmon 26950 . . . . . . . . . . . . . 14 (𝑝 No → dom 𝑝 ∈ On)
4538, 44syl 17 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → dom 𝑝 ∈ On)
46 simprrl 779 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∈ dom 𝑝)
47 onelon 6340 . . . . . . . . . . . . 13 ((dom 𝑝 ∈ On ∧ ∈ dom 𝑝) → ∈ On)
4845, 46, 47syl2anc 584 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∈ On)
49 onsucb 7744 . . . . . . . . . . . 12 ( ∈ On ↔ suc ∈ On)
5048, 49sylib 217 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → suc ∈ On)
51 sltres 26962 . . . . . . . . . . 11 ((𝑈 No 𝑝 No ∧ suc ∈ On) → ((𝑈 ↾ suc ) <s (𝑝 ↾ suc ) → 𝑈 <s 𝑝))
5239, 38, 50, 51syl3anc 1371 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ((𝑈 ↾ suc ) <s (𝑝 ↾ suc ) → 𝑈 <s 𝑝))
5343, 52nsyld 156 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → ¬ (𝑈 ↾ suc ) <s (𝑝 ↾ suc )))
54 noreson 26960 . . . . . . . . . . . . . 14 ((𝑈 No ∧ suc ∈ On) → (𝑈 ↾ suc ) ∈ No )
5539, 50, 54syl2anc 584 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑈 ↾ suc ) ∈ No )
56 sonr 5566 . . . . . . . . . . . . . 14 (( <s Or No ∧ (𝑈 ↾ suc ) ∈ No ) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
5740, 56mpan 688 . . . . . . . . . . . . 13 ((𝑈 ↾ suc ) ∈ No → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
5855, 57syl 17 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
5958adantr 481 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ ¬ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
60 breq2 5107 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑈 → (𝑝 <s 𝑣𝑝 <s 𝑈))
6160notbid 317 . . . . . . . . . . . . . . 15 (𝑣 = 𝑈 → (¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑈))
62 reseq1 5929 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑈 → (𝑣 ↾ suc ) = (𝑈 ↾ suc ))
6362eqeq2d 2748 . . . . . . . . . . . . . . 15 (𝑣 = 𝑈 → ((𝑝 ↾ suc ) = (𝑣 ↾ suc ) ↔ (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
6461, 63imbi12d 344 . . . . . . . . . . . . . 14 (𝑣 = 𝑈 → ((¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )) ↔ (¬ 𝑝 <s 𝑈 → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))))
65 simprrr 780 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
66 simpl3 1193 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑈𝐵)
6764, 65, 66rspcdva 3580 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (¬ 𝑝 <s 𝑈 → (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
6867imp 407 . . . . . . . . . . . 12 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ ¬ 𝑝 <s 𝑈) → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))
6968breq2d 5115 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ ¬ 𝑝 <s 𝑈) → ((𝑈 ↾ suc ) <s (𝑝 ↾ suc ) ↔ (𝑈 ↾ suc ) <s (𝑈 ↾ suc )))
7059, 69mtbird 324 . . . . . . . . . 10 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ ¬ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ) <s (𝑝 ↾ suc ))
7170ex 413 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (¬ 𝑝 <s 𝑈 → ¬ (𝑈 ↾ suc ) <s (𝑝 ↾ suc )))
7253, 71pm2.61d 179 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑈 ↾ suc ) <s (𝑝 ↾ suc ))
73 simpl1 1191 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
74 simpl2 1192 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝐵 No 𝐵𝑉))
751noinfres 27022 . . . . . . . . . 10 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑝𝐵 ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))) → (𝑇 ↾ suc ) = (𝑝 ↾ suc ))
7673, 74, 37, 46, 65, 75syl113anc 1382 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑇 ↾ suc ) = (𝑝 ↾ suc ))
7776breq2d 5115 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ((𝑈 ↾ suc ) <s (𝑇 ↾ suc ) ↔ (𝑈 ↾ suc ) <s (𝑝 ↾ suc )))
7872, 77mtbird 324 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑈 ↾ suc ) <s (𝑇 ↾ suc ))
7978rexlimdvaa 3151 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → (∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))) → ¬ (𝑈 ↾ suc ) <s (𝑇 ↾ suc )))
8035, 79sylbid 239 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ( ∈ dom 𝑇 → ¬ (𝑈 ↾ suc ) <s (𝑇 ↾ suc )))
8180imp 407 . . . 4 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ ∈ dom 𝑇) → ¬ (𝑈 ↾ suc ) <s (𝑇 ↾ suc ))
8221, 81eqnbrtrd 5121 . . 3 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ ∈ dom 𝑇) → ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ) <s (𝑇 ↾ suc ))
8382ralrimiva 3141 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ∀ ∈ dom 𝑇 ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ) <s (𝑇 ↾ suc ))
84 noresle 26997 . 2 (((𝑇 No ∧ (𝑈 ↾ dom 𝑇) ∈ No ) ∧ (dom 𝑇 ⊆ dom 𝑇 ∧ dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇 ∧ ∀ ∈ dom 𝑇 ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ) <s (𝑇 ↾ suc ))) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇)
853, 10, 11, 15, 83, 84syl23anc 1377 1 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  {cab 2714  wral 3062  wrex 3071  cun 3906  cin 3907  wss 3908  ifcif 4484  {csn 4584  cop 4590   class class class wbr 5103  cmpt 5186   Or wor 5542  dom cdm 5631  cres 5633  Ord word 6314  Oncon0 6315  suc csuc 6317  cio 6443  cfv 6493  crio 7306  1oc1o 8397   No csur 26940   <s cslt 26941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5240  ax-sep 5254  ax-nul 5261  ax-pr 5382  ax-un 7664
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4864  df-int 4906  df-iun 4954  df-br 5104  df-opab 5166  df-mpt 5187  df-tr 5221  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6318  df-on 6319  df-suc 6321  df-iota 6445  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7307  df-1o 8404  df-2o 8405  df-no 26943  df-slt 26944  df-bday 26945
This theorem is referenced by:  noinfbnd1lem2  27024  noinfbnd1lem6  27028
  Copyright terms: Public domain W3C validator