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

Theorem noinfbnd1lem1 27783
Description: Lemma for noinfbnd1 27789. 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 27778 . . 3 ((𝐵 No 𝐵𝑉) → 𝑇 No )
323ad2ant2 1133 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝑇 No )
4 simp2l 1198 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝐵 No )
5 simp3 1137 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝑈𝐵)
64, 5sseldd 3996 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → 𝑈 No )
7 nodmon 27710 . . . 4 (𝑇 No → dom 𝑇 ∈ On)
83, 7syl 17 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → dom 𝑇 ∈ On)
9 noreson 27720 . . 3 ((𝑈 No ∧ dom 𝑇 ∈ On) → (𝑈 ↾ dom 𝑇) ∈ No )
106, 8, 9syl2anc 584 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → (𝑈 ↾ dom 𝑇) ∈ No )
11 ssidd 4019 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → dom 𝑇 ⊆ dom 𝑇)
12 dmres 6032 . . . 4 dom (𝑈 ↾ dom 𝑇) = (dom 𝑇 ∩ dom 𝑈)
13 inss1 4245 . . . 4 (dom 𝑇 ∩ dom 𝑈) ⊆ dom 𝑇
1412, 13eqsstri 4030 . . 3 dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇
1514a1i 11 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇)
16 nodmord 27713 . . . . . . . 8 (𝑇 No → Ord dom 𝑇)
173, 16syl 17 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → Ord dom 𝑇)
18 ordsucss 7838 . . . . . . 7 (Ord dom 𝑇 → ( ∈ dom 𝑇 → suc ⊆ dom 𝑇))
1917, 18syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ( ∈ dom 𝑇 → suc ⊆ dom 𝑇))
2019imp 406 . . . . 5 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ ∈ dom 𝑇) → suc ⊆ dom 𝑇)
2120resabs1d 6028 . . . 4 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ ∈ dom 𝑇) → ((𝑈 ↾ dom 𝑇) ↾ suc ) = (𝑈 ↾ suc ))
221noinfdm 27779 . . . . . . . . 9 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = { ∣ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )))})
2322eleq2d 2825 . . . . . . . 8 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( ∈ dom 𝑇 ∈ { ∣ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )))}))
24 abid 2716 . . . . . . . . 9 ( ∈ { ∣ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )))} ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc ))))
25 breq2 5152 . . . . . . . . . . . . . 14 (𝑞 = 𝑣 → (𝑝 <s 𝑞𝑝 <s 𝑣))
2625notbid 318 . . . . . . . . . . . . 13 (𝑞 = 𝑣 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣))
27 reseq1 5994 . . . . . . . . . . . . . 14 (𝑞 = 𝑣 → (𝑞 ↾ suc ) = (𝑣 ↾ suc ))
2827eqeq2d 2746 . . . . . . . . . . . . 13 (𝑞 = 𝑣 → ((𝑝 ↾ suc ) = (𝑞 ↾ suc ) ↔ (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
2926, 28imbi12d 344 . . . . . . . . . . . 12 (𝑞 = 𝑣 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
3029cbvralvw 3235 . . . . . . . . . . 11 (∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )) ↔ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
3130anbi2i 623 . . . . . . . . . 10 (( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc ))) ↔ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
3231rexbii 3092 . . . . . . . . 9 (∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc ))) ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
3324, 32bitri 275 . . . . . . . 8 ( ∈ { ∣ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑞𝐵𝑝 <s 𝑞 → (𝑝 ↾ suc ) = (𝑞 ↾ suc )))} ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))
3423, 33bitrdi 287 . . . . . . 7 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → ( ∈ dom 𝑇 ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
35343ad2ant1 1132 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ( ∈ dom 𝑇 ↔ ∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))))
36 simpl2l 1225 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝐵 No )
37 simprl 771 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑝𝐵)
3836, 37sseldd 3996 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑝 No )
396adantr 480 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑈 No )
40 sltso 27736 . . . . . . . . . . . 12 <s Or No
41 soasym 5629 . . . . . . . . . . . 12 (( <s Or No ∧ (𝑝 No 𝑈 No )) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
4240, 41mpan 690 . . . . . . . . . . 11 ((𝑝 No 𝑈 No ) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
4338, 39, 42syl2anc 584 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝))
44 nodmon 27710 . . . . . . . . . . . . . 14 (𝑝 No → dom 𝑝 ∈ On)
4538, 44syl 17 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → dom 𝑝 ∈ On)
46 simprrl 781 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∈ dom 𝑝)
47 onelon 6411 . . . . . . . . . . . . 13 ((dom 𝑝 ∈ On ∧ ∈ dom 𝑝) → ∈ On)
4845, 46, 47syl2anc 584 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∈ On)
49 onsucb 7837 . . . . . . . . . . . 12 ( ∈ On ↔ suc ∈ On)
5048, 49sylib 218 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → suc ∈ On)
51 sltres 27722 . . . . . . . . . . 11 ((𝑈 No 𝑝 No ∧ suc ∈ On) → ((𝑈 ↾ suc ) <s (𝑝 ↾ suc ) → 𝑈 <s 𝑝))
5239, 38, 50, 51syl3anc 1370 . . . . . . . . . 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 27720 . . . . . . . . . . . . . 14 ((𝑈 No ∧ suc ∈ On) → (𝑈 ↾ suc ) ∈ No )
5539, 50, 54syl2anc 584 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑈 ↾ suc ) ∈ No )
56 sonr 5621 . . . . . . . . . . . . . 14 (( <s Or No ∧ (𝑈 ↾ suc ) ∈ No ) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
5740, 56mpan 690 . . . . . . . . . . . . 13 ((𝑈 ↾ suc ) ∈ No → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
5855, 57syl 17 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
5958adantr 480 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ ¬ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ) <s (𝑈 ↾ suc ))
60 breq2 5152 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑈 → (𝑝 <s 𝑣𝑝 <s 𝑈))
6160notbid 318 . . . . . . . . . . . . . . 15 (𝑣 = 𝑈 → (¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑈))
62 reseq1 5994 . . . . . . . . . . . . . . . 16 (𝑣 = 𝑈 → (𝑣 ↾ suc ) = (𝑈 ↾ suc ))
6362eqeq2d 2746 . . . . . . . . . . . . . . 15 (𝑣 = 𝑈 → ((𝑝 ↾ suc ) = (𝑣 ↾ suc ) ↔ (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
6461, 63imbi12d 344 . . . . . . . . . . . . . 14 (𝑣 = 𝑈 → ((¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )) ↔ (¬ 𝑝 <s 𝑈 → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))))
65 simprrr 782 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))
66 simpl3 1192 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → 𝑈𝐵)
6764, 65, 66rspcdva 3623 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (¬ 𝑝 <s 𝑈 → (𝑝 ↾ suc ) = (𝑈 ↾ suc )))
6867imp 406 . . . . . . . . . . . 12 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ ¬ 𝑝 <s 𝑈) → (𝑝 ↾ suc ) = (𝑈 ↾ suc ))
6968breq2d 5160 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ ¬ 𝑝 <s 𝑈) → ((𝑈 ↾ suc ) <s (𝑝 ↾ suc ) ↔ (𝑈 ↾ suc ) <s (𝑈 ↾ suc )))
7059, 69mtbird 325 . . . . . . . . . 10 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) ∧ ¬ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ) <s (𝑝 ↾ suc ))
7170ex 412 . . . . . . . . 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 1190 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
74 simpl2 1191 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝐵 No 𝐵𝑉))
751noinfres 27782 . . . . . . . . . 10 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑝𝐵 ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc )))) → (𝑇 ↾ suc ) = (𝑝 ↾ suc ))
7673, 74, 37, 46, 65, 75syl113anc 1381 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → (𝑇 ↾ suc ) = (𝑝 ↾ suc ))
7776breq2d 5160 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ((𝑈 ↾ suc ) <s (𝑇 ↾ suc ) ↔ (𝑈 ↾ suc ) <s (𝑝 ↾ suc )))
7872, 77mtbird 325 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ (𝑝𝐵 ∧ ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))))) → ¬ (𝑈 ↾ suc ) <s (𝑇 ↾ suc ))
7978rexlimdvaa 3154 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → (∃𝑝𝐵 ( ∈ dom 𝑝 ∧ ∀𝑣𝐵𝑝 <s 𝑣 → (𝑝 ↾ suc ) = (𝑣 ↾ suc ))) → ¬ (𝑈 ↾ suc ) <s (𝑇 ↾ suc )))
8035, 79sylbid 240 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ( ∈ dom 𝑇 → ¬ (𝑈 ↾ suc ) <s (𝑇 ↾ suc )))
8180imp 406 . . . 4 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ ∈ dom 𝑇) → ¬ (𝑈 ↾ suc ) <s (𝑇 ↾ suc ))
8221, 81eqnbrtrd 5166 . . 3 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) ∧ ∈ dom 𝑇) → ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ) <s (𝑇 ↾ suc ))
8382ralrimiva 3144 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ∀ ∈ dom 𝑇 ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ) <s (𝑇 ↾ suc ))
84 noresle 27757 . 2 (((𝑇 No ∧ (𝑈 ↾ dom 𝑇) ∈ No ) ∧ (dom 𝑇 ⊆ dom 𝑇 ∧ dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇 ∧ ∀ ∈ dom 𝑇 ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ) <s (𝑇 ↾ suc ))) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇)
853, 10, 11, 15, 83, 84syl23anc 1376 1 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ 𝑈𝐵) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  {cab 2712  wral 3059  wrex 3068  cun 3961  cin 3962  wss 3963  ifcif 4531  {csn 4631  cop 4637   class class class wbr 5148  cmpt 5231   Or wor 5596  dom cdm 5689  cres 5691  Ord word 6385  Oncon0 6386  suc csuc 6388  cio 6514  cfv 6563  crio 7387  1oc1o 8498   No csur 27699   <s cslt 27700
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fo 6569  df-fv 6571  df-riota 7388  df-1o 8505  df-2o 8506  df-no 27702  df-slt 27703  df-bday 27704
This theorem is referenced by:  noinfbnd1lem2  27784  noinfbnd1lem6  27788
  Copyright terms: Public domain W3C validator