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

Theorem noinfbnd1lem5 27787
Description: Lemma for noinfbnd1 27789. 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 27778 . . . . . . . 8 ((𝐵 No 𝐵𝑉) → 𝑇 No )
323ad2ant2 1133 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑇 No )
43adantl 481 . . . . . 6 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑇 No )
5 nodmord 27713 . . . . . 6 (𝑇 No → Ord dom 𝑇)
64, 5syl 17 . . . . 5 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → Ord dom 𝑇)
7 ordirr 6404 . . . . 5 (Ord dom 𝑇 → ¬ dom 𝑇 ∈ dom 𝑇)
86, 7syl 17 . . . 4 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ dom 𝑇 ∈ dom 𝑇)
9 simpr3l 1233 . . . . . . . 8 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑈𝐵)
109adantr 480 . . . . . . 7 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → 𝑈𝐵)
11 ndmfv 6942 . . . . . . . . . . 11 (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) = ∅)
12 2on0 8521 . . . . . . . . . . . . 13 2o ≠ ∅
1312necomi 2993 . . . . . . . . . . . 12 ∅ ≠ 2o
14 neeq1 3001 . . . . . . . . . . . 12 ((𝑈‘dom 𝑇) = ∅ → ((𝑈‘dom 𝑇) ≠ 2o ↔ ∅ ≠ 2o))
1513, 14mpbiri 258 . . . . . . . . . . 11 ((𝑈‘dom 𝑇) = ∅ → (𝑈‘dom 𝑇) ≠ 2o)
1611, 15syl 17 . . . . . . . . . 10 (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) ≠ 2o)
1716neneqd 2943 . . . . . . . . 9 (¬ dom 𝑇 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑇) = 2o)
1817con4i 114 . . . . . . . 8 ((𝑈‘dom 𝑇) = 2o → dom 𝑇 ∈ dom 𝑈)
1918adantl 481 . . . . . . 7 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 ∈ dom 𝑈)
20 simpl2l 1225 . . . . . . . . . . . . . . . . 17 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) → 𝐵 No )
2120adantr 480 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝐵 No )
22 simpl3l 1227 . . . . . . . . . . . . . . . . 17 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) → 𝑈𝐵)
2322adantr 480 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝑈𝐵)
2421, 23sseldd 3996 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝑈 No )
25 nofun 27709 . . . . . . . . . . . . . . 15 (𝑈 No → Fun 𝑈)
2624, 25syl 17 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → Fun 𝑈)
27 simprll 779 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝑧𝐵)
2821, 27sseldd 3996 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝑧 No )
29 nofun 27709 . . . . . . . . . . . . . . 15 (𝑧 No → Fun 𝑧)
3028, 29syl 17 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → Fun 𝑧)
31 simpl3r 1228 . . . . . . . . . . . . . . . 16 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) → (𝑈 ↾ dom 𝑇) = 𝑇)
3231adantr 480 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈 ↾ dom 𝑇) = 𝑇)
33 simpll1 1211 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
34 simpll2 1212 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝐵 No 𝐵𝑉))
35 simpll3 1213 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
36 simprl 771 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧))
371noinfbnd1lem2 27784 . . . . . . . . . . . . . . . 16 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ ((𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇) ∧ (𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧))) → (𝑧 ↾ dom 𝑇) = 𝑇)
3833, 34, 35, 36, 37syl112anc 1373 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑧 ↾ dom 𝑇) = 𝑇)
3932, 38eqtr4d 2778 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈 ↾ dom 𝑇) = (𝑧 ↾ dom 𝑇))
40 simplr 769 . . . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑧‘dom 𝑇) = 2o)
43 ndmfv 6942 . . . . . . . . . . . . . . . . . 18 (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) = ∅)
44 neeq1 3001 . . . . . . . . . . . . . . . . . . 19 ((𝑧‘dom 𝑇) = ∅ → ((𝑧‘dom 𝑇) ≠ 2o ↔ ∅ ≠ 2o))
4513, 44mpbiri 258 . . . . . . . . . . . . . . . . . 18 ((𝑧‘dom 𝑇) = ∅ → (𝑧‘dom 𝑇) ≠ 2o)
4643, 45syl 17 . . . . . . . . . . . . . . . . 17 (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) ≠ 2o)
4746neneqd 2943 . . . . . . . . . . . . . . . 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 2778 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))
51 eqfunressuc 7381 . . . . . . . . . . . . . 14 (((Fun 𝑈 ∧ Fun 𝑧) ∧ (𝑈 ↾ dom 𝑇) = (𝑧 ↾ dom 𝑇) ∧ (dom 𝑇 ∈ dom 𝑈 ∧ dom 𝑇 ∈ dom 𝑧 ∧ (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))) → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))
5226, 30, 39, 41, 49, 50, 51syl213anc 1388 . . . . . . . . . . . . 13 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))
5352expr 456 . . . . . . . . . . . 12 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ (𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧)) → ((𝑧‘dom 𝑇) = 2o → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
5453expr 456 . . . . . . . . . . 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 407 . . . . . . . 8 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o)) → ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
5857anassrs 467 . . . . . . 7 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
59 dmeq 5917 . . . . . . . . . 10 (𝑝 = 𝑈 → dom 𝑝 = dom 𝑈)
6059eleq2d 2825 . . . . . . . . 9 (𝑝 = 𝑈 → (dom 𝑇 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑈))
61 breq1 5151 . . . . . . . . . . . 12 (𝑝 = 𝑈 → (𝑝 <s 𝑧𝑈 <s 𝑧))
6261notbid 318 . . . . . . . . . . 11 (𝑝 = 𝑈 → (¬ 𝑝 <s 𝑧 ↔ ¬ 𝑈 <s 𝑧))
63 reseq1 5994 . . . . . . . . . . . 12 (𝑝 = 𝑈 → (𝑝 ↾ suc dom 𝑇) = (𝑈 ↾ suc dom 𝑇))
6463eqeq1d 2737 . . . . . . . . . . 11 (𝑝 = 𝑈 → ((𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇) ↔ (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
6562, 64imbi12d 344 . . . . . . . . . 10 (𝑝 = 𝑈 → ((¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)) ↔ (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
6665ralbidv 3176 . . . . . . . . 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 3622 . . . . . . 7 ((𝑈𝐵 ∧ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))) → ∃𝑝𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
6910, 19, 58, 68syl12anc 837 . . . . . 6 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → ∃𝑝𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
70 nodmon 27710 . . . . . . . . 9 (𝑇 No → dom 𝑇 ∈ On)
714, 70syl 17 . . . . . . . 8 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → dom 𝑇 ∈ On)
7271adantr 480 . . . . . . 7 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 ∈ On)
73 eleq1 2827 . . . . . . . . . 10 (𝑎 = dom 𝑇 → (𝑎 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑝))
74 suceq 6452 . . . . . . . . . . . . . 14 (𝑎 = dom 𝑇 → suc 𝑎 = suc dom 𝑇)
7574reseq2d 6000 . . . . . . . . . . . . 13 (𝑎 = dom 𝑇 → (𝑝 ↾ suc 𝑎) = (𝑝 ↾ suc dom 𝑇))
7674reseq2d 6000 . . . . . . . . . . . . 13 (𝑎 = dom 𝑇 → (𝑧 ↾ suc 𝑎) = (𝑧 ↾ suc dom 𝑇))
7775, 76eqeq12d 2751 . . . . . . . . . . . 12 (𝑎 = dom 𝑇 → ((𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎) ↔ (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
7877imbi2d 340 . . . . . . . . . . 11 (𝑎 = dom 𝑇 → ((¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
7978ralbidv 3176 . . . . . . . . . 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 3177 . . . . . . . 8 (𝑎 = dom 𝑇 → (∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ ∃𝑝𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
8281elabg 3677 . . . . . . 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 27779 . . . . . . . . 9 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
86853ad2ant1 1132 . . . . . . . 8 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → dom 𝑇 = {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
8786adantl 481 . . . . . . 7 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → dom 𝑇 = {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
8887adantr 480 . . . . . 6 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 = {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
8988eleq2d 2825 . . . . 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 816 . . 3 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑈‘dom 𝑇) = 2o)
9291neqned 2945 . 2 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2o)
93 rexanali 3100 . . 3 (∃𝑧𝐵𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2o) ↔ ¬ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o))
94 simpr1 1193 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
95 simpr2 1194 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝐵 No 𝐵𝑉))
96 simplll 775 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧𝐵)
97 simpr3 1195 . . . . . . . . . . . 12 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
98 simpll 767 . . . . . . . . . . . 12 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧))
9994, 95, 97, 98, 37syl112anc 1373 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧 ↾ dom 𝑇) = 𝑇)
1001noinfbnd1lem4 27786 . . . . . . . . . . 11 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑧𝐵 ∧ (𝑧 ↾ dom 𝑇) = 𝑇)) → (𝑧‘dom 𝑇) ≠ ∅)
10194, 95, 96, 99, 100syl112anc 1373 . . . . . . . . . 10 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧‘dom 𝑇) ≠ ∅)
102101neneqd 2943 . . . . . . . . 9 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = ∅)
103102pm2.21d 121 . . . . . . . 8 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ → (𝑈‘dom 𝑇) ≠ 2o))
1041noinfbnd1lem3 27785 . . . . . . . . . . 11 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑧𝐵 ∧ (𝑧 ↾ dom 𝑇) = 𝑇)) → (𝑧‘dom 𝑇) ≠ 1o)
10594, 95, 96, 99, 104syl112anc 1373 . . . . . . . . . 10 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧‘dom 𝑇) ≠ 1o)
106105neneqd 2943 . . . . . . . . 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 769 . . . . . . . . 9 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = 2o)
109 simpr2l 1231 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝐵 No )
110109, 96sseldd 3996 . . . . . . . . . 10 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧 No )
111 nofv 27717 . . . . . . . . . 10 (𝑧 No → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1o ∨ (𝑧‘dom 𝑇) = 2o))
112110, 111syl 17 . . . . . . . . 9 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1o ∨ (𝑧‘dom 𝑇) = 2o))
113 3orel3 1485 . . . . . . . . 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 860 . . . . . . 7 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2o)
116115ex 412 . . . . . 6 (((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) → ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2o))
117116anasss 466 . . . . 5 ((𝑧𝐵 ∧ (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2o)) → ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2o))
118117rexlimiva 3145 . . . 4 (∃𝑧𝐵𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2o) → ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2o))
119118imp 406 . . 3 ((∃𝑧𝐵𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2o)
12093, 119sylanbr 582 . 2 ((¬ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2o)
12192, 120pm2.61ian 812 1 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2o)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3o 1085  w3a 1086   = wceq 1537  wcel 2106  {cab 2712  wne 2938  wral 3059  wrex 3068  cun 3961  wss 3963  c0 4339  ifcif 4531  {csn 4631  cop 4637   class class class wbr 5148  cmpt 5231  dom cdm 5689  cres 5691  Ord word 6385  Oncon0 6386  suc csuc 6388  cio 6514  Fun wfun 6557  cfv 6563  crio 7387  1oc1o 8498  2oc2o 8499   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:  noinfbnd1lem6  27788
  Copyright terms: Public domain W3C validator