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

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

Proof of Theorem noinfbnd1lem5
Dummy variables 𝑝 𝑧 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 noinfbnd1.1 . . . . . . . . 9 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
21noinfno 27082 . . . . . . . 8 ((𝐵 No 𝐵𝑉) → 𝑇 No )
323ad2ant2 1135 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑇 No )
43adantl 483 . . . . . 6 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑇 No )
5 nodmord 27017 . . . . . 6 (𝑇 No → Ord dom 𝑇)
64, 5syl 17 . . . . 5 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → Ord dom 𝑇)
7 ordirr 6340 . . . . 5 (Ord dom 𝑇 → ¬ dom 𝑇 ∈ dom 𝑇)
86, 7syl 17 . . . 4 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ dom 𝑇 ∈ dom 𝑇)
9 simpr3l 1235 . . . . . . . 8 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑈𝐵)
109adantr 482 . . . . . . 7 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → 𝑈𝐵)
11 ndmfv 6882 . . . . . . . . . . 11 (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) = ∅)
12 2on0 8433 . . . . . . . . . . . . 13 2o ≠ ∅
1312necomi 2999 . . . . . . . . . . . 12 ∅ ≠ 2o
14 neeq1 3007 . . . . . . . . . . . 12 ((𝑈‘dom 𝑇) = ∅ → ((𝑈‘dom 𝑇) ≠ 2o ↔ ∅ ≠ 2o))
1513, 14mpbiri 258 . . . . . . . . . . 11 ((𝑈‘dom 𝑇) = ∅ → (𝑈‘dom 𝑇) ≠ 2o)
1611, 15syl 17 . . . . . . . . . 10 (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) ≠ 2o)
1716neneqd 2949 . . . . . . . . 9 (¬ dom 𝑇 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑇) = 2o)
1817con4i 114 . . . . . . . 8 ((𝑈‘dom 𝑇) = 2o → dom 𝑇 ∈ dom 𝑈)
1918adantl 483 . . . . . . 7 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 ∈ dom 𝑈)
20 simpl2l 1227 . . . . . . . . . . . . . . . . 17 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) → 𝐵 No )
2120adantr 482 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝐵 No )
22 simpl3l 1229 . . . . . . . . . . . . . . . . 17 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) → 𝑈𝐵)
2322adantr 482 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝑈𝐵)
2421, 23sseldd 3950 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝑈 No )
25 nofun 27013 . . . . . . . . . . . . . . 15 (𝑈 No → Fun 𝑈)
2624, 25syl 17 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → Fun 𝑈)
27 simprll 778 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝑧𝐵)
2821, 27sseldd 3950 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝑧 No )
29 nofun 27013 . . . . . . . . . . . . . . 15 (𝑧 No → Fun 𝑧)
3028, 29syl 17 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → Fun 𝑧)
31 simpl3r 1230 . . . . . . . . . . . . . . . 16 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) → (𝑈 ↾ dom 𝑇) = 𝑇)
3231adantr 482 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈 ↾ dom 𝑇) = 𝑇)
33 simpll1 1213 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
34 simpll2 1214 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝐵 No 𝐵𝑉))
35 simpll3 1215 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
36 simprl 770 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧))
371noinfbnd1lem2 27088 . . . . . . . . . . . . . . . 16 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ ((𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇) ∧ (𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧))) → (𝑧 ↾ dom 𝑇) = 𝑇)
3833, 34, 35, 36, 37syl112anc 1375 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑧 ↾ dom 𝑇) = 𝑇)
3932, 38eqtr4d 2780 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈 ↾ dom 𝑇) = (𝑧 ↾ dom 𝑇))
40 simplr 768 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈‘dom 𝑇) = 2o)
4140, 18syl 17 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → dom 𝑇 ∈ dom 𝑈)
42 simprr 772 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑧‘dom 𝑇) = 2o)
43 ndmfv 6882 . . . . . . . . . . . . . . . . . 18 (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) = ∅)
44 neeq1 3007 . . . . . . . . . . . . . . . . . . 19 ((𝑧‘dom 𝑇) = ∅ → ((𝑧‘dom 𝑇) ≠ 2o ↔ ∅ ≠ 2o))
4513, 44mpbiri 258 . . . . . . . . . . . . . . . . . 18 ((𝑧‘dom 𝑇) = ∅ → (𝑧‘dom 𝑇) ≠ 2o)
4643, 45syl 17 . . . . . . . . . . . . . . . . 17 (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) ≠ 2o)
4746neneqd 2949 . . . . . . . . . . . . . . . 16 (¬ dom 𝑇 ∈ dom 𝑧 → ¬ (𝑧‘dom 𝑇) = 2o)
4847con4i 114 . . . . . . . . . . . . . . 15 ((𝑧‘dom 𝑇) = 2o → dom 𝑇 ∈ dom 𝑧)
4942, 48syl 17 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → dom 𝑇 ∈ dom 𝑧)
5040, 42eqtr4d 2780 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))
51 eqfunressuc 7311 . . . . . . . . . . . . . 14 (((Fun 𝑈 ∧ Fun 𝑧) ∧ (𝑈 ↾ dom 𝑇) = (𝑧 ↾ dom 𝑇) ∧ (dom 𝑇 ∈ dom 𝑈 ∧ dom 𝑇 ∈ dom 𝑧 ∧ (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))) → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))
5226, 30, 39, 41, 49, 50, 51syl213anc 1390 . . . . . . . . . . . . 13 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))
5352expr 458 . . . . . . . . . . . 12 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ (𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧)) → ((𝑧‘dom 𝑇) = 2o → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
5453expr 458 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ 𝑧𝐵) → (¬ 𝑈 <s 𝑧 → ((𝑧‘dom 𝑇) = 2o → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
5554a2d 29 . . . . . . . . . 10 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ 𝑧𝐵) → ((¬ 𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) → (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
5655ralimdva 3165 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) → (∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) → ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
5756impcom 409 . . . . . . . 8 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o)) → ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
5857anassrs 469 . . . . . . 7 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
59 dmeq 5864 . . . . . . . . . 10 (𝑝 = 𝑈 → dom 𝑝 = dom 𝑈)
6059eleq2d 2824 . . . . . . . . 9 (𝑝 = 𝑈 → (dom 𝑇 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑈))
61 breq1 5113 . . . . . . . . . . . 12 (𝑝 = 𝑈 → (𝑝 <s 𝑧𝑈 <s 𝑧))
6261notbid 318 . . . . . . . . . . 11 (𝑝 = 𝑈 → (¬ 𝑝 <s 𝑧 ↔ ¬ 𝑈 <s 𝑧))
63 reseq1 5936 . . . . . . . . . . . 12 (𝑝 = 𝑈 → (𝑝 ↾ suc dom 𝑇) = (𝑈 ↾ suc dom 𝑇))
6463eqeq1d 2739 . . . . . . . . . . 11 (𝑝 = 𝑈 → ((𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇) ↔ (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
6562, 64imbi12d 345 . . . . . . . . . 10 (𝑝 = 𝑈 → ((¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)) ↔ (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
6665ralbidv 3175 . . . . . . . . 9 (𝑝 = 𝑈 → (∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)) ↔ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
6760, 66anbi12d 632 . . . . . . . 8 (𝑝 = 𝑈 → ((dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))) ↔ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
6867rspcev 3584 . . . . . . 7 ((𝑈𝐵 ∧ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))) → ∃𝑝𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
6910, 19, 58, 68syl12anc 836 . . . . . 6 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → ∃𝑝𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
70 nodmon 27014 . . . . . . . . 9 (𝑇 No → dom 𝑇 ∈ On)
714, 70syl 17 . . . . . . . 8 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → dom 𝑇 ∈ On)
7271adantr 482 . . . . . . 7 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 ∈ On)
73 eleq1 2826 . . . . . . . . . 10 (𝑎 = dom 𝑇 → (𝑎 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑝))
74 suceq 6388 . . . . . . . . . . . . . 14 (𝑎 = dom 𝑇 → suc 𝑎 = suc dom 𝑇)
7574reseq2d 5942 . . . . . . . . . . . . 13 (𝑎 = dom 𝑇 → (𝑝 ↾ suc 𝑎) = (𝑝 ↾ suc dom 𝑇))
7674reseq2d 5942 . . . . . . . . . . . . 13 (𝑎 = dom 𝑇 → (𝑧 ↾ suc 𝑎) = (𝑧 ↾ suc dom 𝑇))
7775, 76eqeq12d 2753 . . . . . . . . . . . 12 (𝑎 = dom 𝑇 → ((𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎) ↔ (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
7877imbi2d 341 . . . . . . . . . . 11 (𝑎 = dom 𝑇 → ((¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
7978ralbidv 3175 . . . . . . . . . 10 (𝑎 = dom 𝑇 → (∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
8073, 79anbi12d 632 . . . . . . . . 9 (𝑎 = dom 𝑇 → ((𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
8180rexbidv 3176 . . . . . . . 8 (𝑎 = dom 𝑇 → (∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ ∃𝑝𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
8281elabg 3633 . . . . . . 7 (dom 𝑇 ∈ On → (dom 𝑇 ∈ {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))} ↔ ∃𝑝𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
8372, 82syl 17 . . . . . 6 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → (dom 𝑇 ∈ {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))} ↔ ∃𝑝𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
8469, 83mpbird 257 . . . . 5 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 ∈ {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
851noinfdm 27083 . . . . . . . . 9 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
86853ad2ant1 1134 . . . . . . . 8 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → dom 𝑇 = {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
8786adantl 483 . . . . . . 7 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → dom 𝑇 = {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
8887adantr 482 . . . . . 6 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 = {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
8988eleq2d 2824 . . . . 5 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → (dom 𝑇 ∈ dom 𝑇 ↔ dom 𝑇 ∈ {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))}))
9084, 89mpbird 257 . . . 4 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 ∈ dom 𝑇)
918, 90mtand 815 . . 3 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑈‘dom 𝑇) = 2o)
9291neqned 2951 . 2 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2o)
93 rexanali 3106 . . 3 (∃𝑧𝐵𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2o) ↔ ¬ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o))
94 simpr1 1195 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
95 simpr2 1196 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝐵 No 𝐵𝑉))
96 simplll 774 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧𝐵)
97 simpr3 1197 . . . . . . . . . . . 12 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
98 simpll 766 . . . . . . . . . . . 12 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧))
9994, 95, 97, 98, 37syl112anc 1375 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧 ↾ dom 𝑇) = 𝑇)
1001noinfbnd1lem4 27090 . . . . . . . . . . 11 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑧𝐵 ∧ (𝑧 ↾ dom 𝑇) = 𝑇)) → (𝑧‘dom 𝑇) ≠ ∅)
10194, 95, 96, 99, 100syl112anc 1375 . . . . . . . . . 10 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧‘dom 𝑇) ≠ ∅)
102101neneqd 2949 . . . . . . . . 9 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = ∅)
103102pm2.21d 121 . . . . . . . 8 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ → (𝑈‘dom 𝑇) ≠ 2o))
1041noinfbnd1lem3 27089 . . . . . . . . . . 11 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑧𝐵 ∧ (𝑧 ↾ dom 𝑇) = 𝑇)) → (𝑧‘dom 𝑇) ≠ 1o)
10594, 95, 96, 99, 104syl112anc 1375 . . . . . . . . . 10 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧‘dom 𝑇) ≠ 1o)
106105neneqd 2949 . . . . . . . . 9 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = 1o)
107106pm2.21d 121 . . . . . . . 8 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = 1o → (𝑈‘dom 𝑇) ≠ 2o))
108 simplr 768 . . . . . . . . 9 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = 2o)
109 simpr2l 1233 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝐵 No )
110109, 96sseldd 3950 . . . . . . . . . 10 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧 No )
111 nofv 27021 . . . . . . . . . 10 (𝑧 No → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1o ∨ (𝑧‘dom 𝑇) = 2o))
112110, 111syl 17 . . . . . . . . 9 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1o ∨ (𝑧‘dom 𝑇) = 2o))
113 3orel3 1487 . . . . . . . . 9 (¬ (𝑧‘dom 𝑇) = 2o → (((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1o ∨ (𝑧‘dom 𝑇) = 2o) → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1o)))
114108, 112, 113sylc 65 . . . . . . . 8 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1o))
115103, 107, 114mpjaod 859 . . . . . . 7 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2o)
116115ex 414 . . . . . 6 (((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) → ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2o))
117116anasss 468 . . . . 5 ((𝑧𝐵 ∧ (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2o)) → ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2o))
118117rexlimiva 3145 . . . 4 (∃𝑧𝐵𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2o) → ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2o))
119118imp 408 . . 3 ((∃𝑧𝐵𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2o)
12093, 119sylanbr 583 . 2 ((¬ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2o)
12192, 120pm2.61ian 811 1 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2o)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3o 1087  w3a 1088   = wceq 1542  wcel 2107  {cab 2714  wne 2944  wral 3065  wrex 3074  cun 3913  wss 3915  c0 4287  ifcif 4491  {csn 4591  cop 4597   class class class wbr 5110  cmpt 5193  dom cdm 5638  cres 5640  Ord word 6321  Oncon0 6322  suc csuc 6324  cio 6451  Fun wfun 6495  cfv 6501  crio 7317  1oc1o 8410  2oc2o 8411   No csur 27004   <s cslt 27005
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6325  df-on 6326  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-1o 8417  df-2o 8418  df-no 27007  df-slt 27008  df-bday 27009
This theorem is referenced by:  noinfbnd1lem6  27092
  Copyright terms: Public domain W3C validator