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

Theorem noinfbnd1lem4 27675
Description: Lemma for noinfbnd1 27678. If 𝑈 is a prolongment of 𝑇 and in 𝐵, then (𝑈‘dom 𝑇) is not undefined. (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
noinfbnd1lem4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ ∅)
Distinct variable groups:   𝐵,𝑔,𝑢,𝑣,𝑥,𝑦   𝑣,𝑈   𝑥,𝑢,𝑦   𝑔,𝑉   𝑥,𝑣,𝑦,𝑈
Allowed substitution hints:   𝑇(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑈(𝑢,𝑔)   𝑉(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem noinfbnd1lem4
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 simpl1 1188 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤𝐵𝑤 <s 𝑈)) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
2 simpl2 1189 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝐵 No 𝐵𝑉))
3 simprl 769 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤𝐵𝑤 <s 𝑈)) → 𝑤𝐵)
4 simpl3 1190 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
5 simp2l 1196 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝐵 No )
65sselda 3972 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤𝐵) → 𝑤 No )
7 simp3l 1198 . . . . . . . . . . . . . 14 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑈𝐵)
85, 7sseldd 3973 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑈 No )
98adantr 479 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤𝐵) → 𝑈 No )
10 sltso 27625 . . . . . . . . . . . . 13 <s Or No
11 soasym 5615 . . . . . . . . . . . . 13 (( <s Or No ∧ (𝑤 No 𝑈 No )) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤))
1210, 11mpan 688 . . . . . . . . . . . 12 ((𝑤 No 𝑈 No ) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤))
136, 9, 12syl2anc 582 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤𝐵) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤))
1413impr 453 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤𝐵𝑤 <s 𝑈)) → ¬ 𝑈 <s 𝑤)
153, 14jca 510 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝑤𝐵 ∧ ¬ 𝑈 <s 𝑤))
16 noinfbnd1.1 . . . . . . . . . 10 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
1716noinfbnd1lem2 27673 . . . . . . . . 9 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ ((𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇) ∧ (𝑤𝐵 ∧ ¬ 𝑈 <s 𝑤))) → (𝑤 ↾ dom 𝑇) = 𝑇)
181, 2, 4, 15, 17syl112anc 1371 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝑤 ↾ dom 𝑇) = 𝑇)
1916noinfbnd1lem3 27674 . . . . . . . 8 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑤𝐵 ∧ (𝑤 ↾ dom 𝑇) = 𝑇)) → (𝑤‘dom 𝑇) ≠ 1o)
201, 2, 3, 18, 19syl112anc 1371 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝑤‘dom 𝑇) ≠ 1o)
2120neneqd 2935 . . . . . 6 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤𝐵𝑤 <s 𝑈)) → ¬ (𝑤‘dom 𝑇) = 1o)
2221expr 455 . . . . 5 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤𝐵) → (𝑤 <s 𝑈 → ¬ (𝑤‘dom 𝑇) = 1o))
23 imnan 398 . . . . 5 ((𝑤 <s 𝑈 → ¬ (𝑤‘dom 𝑇) = 1o) ↔ ¬ (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1o))
2422, 23sylib 217 . . . 4 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤𝐵) → ¬ (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1o))
2524nrexdv 3139 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → ¬ ∃𝑤𝐵 (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1o))
26 breq2 5147 . . . . . . 7 (𝑥 = 𝑈 → (𝑦 <s 𝑥𝑦 <s 𝑈))
2726rexbidv 3169 . . . . . 6 (𝑥 = 𝑈 → (∃𝑦𝐵 𝑦 <s 𝑥 ↔ ∃𝑦𝐵 𝑦 <s 𝑈))
28 simpl1 1188 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
29 dfral2 3089 . . . . . . . 8 (∀𝑥𝐵𝑦𝐵 𝑦 <s 𝑥 ↔ ¬ ∃𝑥𝐵 ¬ ∃𝑦𝐵 𝑦 <s 𝑥)
30 ralnex 3062 . . . . . . . . 9 (∀𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ ¬ ∃𝑦𝐵 𝑦 <s 𝑥)
3130rexbii 3084 . . . . . . . 8 (∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ↔ ∃𝑥𝐵 ¬ ∃𝑦𝐵 𝑦 <s 𝑥)
3229, 31xchbinxr 334 . . . . . . 7 (∀𝑥𝐵𝑦𝐵 𝑦 <s 𝑥 ↔ ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
3328, 32sylibr 233 . . . . . 6 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∀𝑥𝐵𝑦𝐵 𝑦 <s 𝑥)
34 simpl3l 1225 . . . . . 6 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → 𝑈𝐵)
3527, 33, 34rspcdva 3603 . . . . 5 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∃𝑦𝐵 𝑦 <s 𝑈)
36 breq1 5146 . . . . . 6 (𝑦 = 𝑤 → (𝑦 <s 𝑈𝑤 <s 𝑈))
3736cbvrexvw 3226 . . . . 5 (∃𝑦𝐵 𝑦 <s 𝑈 ↔ ∃𝑤𝐵 𝑤 <s 𝑈)
3835, 37sylib 217 . . . 4 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∃𝑤𝐵 𝑤 <s 𝑈)
39 simpl2l 1223 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → 𝐵 No )
4039adantr 479 . . . . . . . . 9 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → 𝐵 No )
41 simprl 769 . . . . . . . . 9 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → 𝑤𝐵)
4240, 41sseldd 3973 . . . . . . . 8 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → 𝑤 No )
4334adantr 479 . . . . . . . . 9 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → 𝑈𝐵)
4440, 43sseldd 3973 . . . . . . . 8 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → 𝑈 No )
45 simpl2 1189 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → (𝐵 No 𝐵𝑉))
4616noinfno 27667 . . . . . . . . . . 11 ((𝐵 No 𝐵𝑉) → 𝑇 No )
4745, 46syl 17 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → 𝑇 No )
4847adantr 479 . . . . . . . . 9 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → 𝑇 No )
49 nodmon 27599 . . . . . . . . 9 (𝑇 No → dom 𝑇 ∈ On)
5048, 49syl 17 . . . . . . . 8 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → dom 𝑇 ∈ On)
51 simpll1 1209 . . . . . . . . . 10 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
52 simpll2 1210 . . . . . . . . . 10 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝐵 No 𝐵𝑉))
53 simpll3 1211 . . . . . . . . . 10 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
54 simprr 771 . . . . . . . . . . . 12 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → 𝑤 <s 𝑈)
5542, 44, 12syl2anc 582 . . . . . . . . . . . 12 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤))
5654, 55mpd 15 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → ¬ 𝑈 <s 𝑤)
5741, 56jca 510 . . . . . . . . . 10 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝑤𝐵 ∧ ¬ 𝑈 <s 𝑤))
5851, 52, 53, 57, 17syl112anc 1371 . . . . . . . . 9 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝑤 ↾ dom 𝑇) = 𝑇)
59 simpl3r 1226 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → (𝑈 ↾ dom 𝑇) = 𝑇)
6059adantr 479 . . . . . . . . 9 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝑈 ↾ dom 𝑇) = 𝑇)
6158, 60eqtr4d 2768 . . . . . . . 8 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝑤 ↾ dom 𝑇) = (𝑈 ↾ dom 𝑇))
62 simplr 767 . . . . . . . 8 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝑈‘dom 𝑇) = ∅)
63 nogt01o 27645 . . . . . . . 8 (((𝑤 No 𝑈 No ∧ dom 𝑇 ∈ On) ∧ ((𝑤 ↾ dom 𝑇) = (𝑈 ↾ dom 𝑇) ∧ 𝑤 <s 𝑈) ∧ (𝑈‘dom 𝑇) = ∅) → (𝑤‘dom 𝑇) = 1o)
6442, 44, 50, 61, 54, 62, 63syl321anc 1389 . . . . . . 7 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤𝐵𝑤 <s 𝑈)) → (𝑤‘dom 𝑇) = 1o)
6564expr 455 . . . . . 6 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ 𝑤𝐵) → (𝑤 <s 𝑈 → (𝑤‘dom 𝑇) = 1o))
6665ancld 549 . . . . 5 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ 𝑤𝐵) → (𝑤 <s 𝑈 → (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1o)))
6766reximdva 3158 . . . 4 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → (∃𝑤𝐵 𝑤 <s 𝑈 → ∃𝑤𝐵 (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1o)))
6838, 67mpd 15 . . 3 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∃𝑤𝐵 (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1o))
6925, 68mtand 814 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → ¬ (𝑈‘dom 𝑇) = ∅)
7069neqned 2937 1 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  w3a 1084   = wceq 1533  wcel 2098  {cab 2702  wne 2930  wral 3051  wrex 3060  cun 3938  wss 3940  c0 4318  ifcif 4524  {csn 4624  cop 4630   class class class wbr 5143  cmpt 5226   Or wor 5583  dom cdm 5672  cres 5674  Oncon0 6364  suc csuc 6366  cio 6492  cfv 6542  crio 7370  1oc1o 8476   No csur 27589   <s cslt 27590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pr 5423  ax-un 7737
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3960  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6367  df-on 6368  df-suc 6370  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7371  df-1o 8483  df-2o 8484  df-no 27592  df-slt 27593  df-bday 27594
This theorem is referenced by:  noinfbnd1lem5  27676  noinfbnd1lem6  27677
  Copyright terms: Public domain W3C validator