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

Theorem noinfbnd1lem5 27075
Description: Lemma for noinfbnd1 27077. 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 27066 . . . . . . . 8 ((𝐵 No 𝐵𝑉) → 𝑇 No )
323ad2ant2 1134 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑇 No )
43adantl 482 . . . . . 6 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑇 No )
5 nodmord 27001 . . . . . 6 (𝑇 No → Ord dom 𝑇)
64, 5syl 17 . . . . 5 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → Ord dom 𝑇)
7 ordirr 6335 . . . . 5 (Ord dom 𝑇 → ¬ dom 𝑇 ∈ dom 𝑇)
86, 7syl 17 . . . 4 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ dom 𝑇 ∈ dom 𝑇)
9 simpr3l 1234 . . . . . . . 8 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑈𝐵)
109adantr 481 . . . . . . 7 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → 𝑈𝐵)
11 ndmfv 6877 . . . . . . . . . . 11 (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) = ∅)
12 2on0 8428 . . . . . . . . . . . . 13 2o ≠ ∅
1312necomi 2998 . . . . . . . . . . . 12 ∅ ≠ 2o
14 neeq1 3006 . . . . . . . . . . . 12 ((𝑈‘dom 𝑇) = ∅ → ((𝑈‘dom 𝑇) ≠ 2o ↔ ∅ ≠ 2o))
1513, 14mpbiri 257 . . . . . . . . . . 11 ((𝑈‘dom 𝑇) = ∅ → (𝑈‘dom 𝑇) ≠ 2o)
1611, 15syl 17 . . . . . . . . . 10 (¬ dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) ≠ 2o)
1716neneqd 2948 . . . . . . . . 9 (¬ dom 𝑇 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑇) = 2o)
1817con4i 114 . . . . . . . 8 ((𝑈‘dom 𝑇) = 2o → dom 𝑇 ∈ dom 𝑈)
1918adantl 482 . . . . . . 7 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 ∈ dom 𝑈)
20 simpl2l 1226 . . . . . . . . . . . . . . . . 17 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) → 𝐵 No )
2120adantr 481 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝐵 No )
22 simpl3l 1228 . . . . . . . . . . . . . . . . 17 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) → 𝑈𝐵)
2322adantr 481 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝑈𝐵)
2421, 23sseldd 3945 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝑈 No )
25 nofun 26997 . . . . . . . . . . . . . . 15 (𝑈 No → Fun 𝑈)
2624, 25syl 17 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → Fun 𝑈)
27 simprll 777 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝑧𝐵)
2821, 27sseldd 3945 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → 𝑧 No )
29 nofun 26997 . . . . . . . . . . . . . . 15 (𝑧 No → Fun 𝑧)
3028, 29syl 17 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → Fun 𝑧)
31 simpl3r 1229 . . . . . . . . . . . . . . . 16 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) → (𝑈 ↾ dom 𝑇) = 𝑇)
3231adantr 481 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈 ↾ dom 𝑇) = 𝑇)
33 simpll1 1212 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
34 simpll2 1213 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝐵 No 𝐵𝑉))
35 simpll3 1214 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
36 simprl 769 . . . . . . . . . . . . . . . 16 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧))
371noinfbnd1lem2 27072 . . . . . . . . . . . . . . . 16 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ ((𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇) ∧ (𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧))) → (𝑧 ↾ dom 𝑇) = 𝑇)
3833, 34, 35, 36, 37syl112anc 1374 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑧 ↾ dom 𝑇) = 𝑇)
3932, 38eqtr4d 2779 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈 ↾ dom 𝑇) = (𝑧 ↾ dom 𝑇))
40 simplr 767 . . . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑧‘dom 𝑇) = 2o)
43 ndmfv 6877 . . . . . . . . . . . . . . . . . 18 (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) = ∅)
44 neeq1 3006 . . . . . . . . . . . . . . . . . . 19 ((𝑧‘dom 𝑇) = ∅ → ((𝑧‘dom 𝑇) ≠ 2o ↔ ∅ ≠ 2o))
4513, 44mpbiri 257 . . . . . . . . . . . . . . . . . 18 ((𝑧‘dom 𝑇) = ∅ → (𝑧‘dom 𝑇) ≠ 2o)
4643, 45syl 17 . . . . . . . . . . . . . . . . 17 (¬ dom 𝑇 ∈ dom 𝑧 → (𝑧‘dom 𝑇) ≠ 2o)
4746neneqd 2948 . . . . . . . . . . . . . . . 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 2779 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))
51 eqfunressuc 7306 . . . . . . . . . . . . . 14 (((Fun 𝑈 ∧ Fun 𝑧) ∧ (𝑈 ↾ dom 𝑇) = (𝑧 ↾ dom 𝑇) ∧ (dom 𝑇 ∈ dom 𝑈 ∧ dom 𝑇 ∈ dom 𝑧 ∧ (𝑈‘dom 𝑇) = (𝑧‘dom 𝑇))) → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))
5226, 30, 39, 41, 49, 50, 51syl213anc 1389 . . . . . . . . . . . . 13 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ ((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ (𝑧‘dom 𝑇) = 2o)) → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))
5352expr 457 . . . . . . . . . . . 12 ((((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) ∧ (𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧)) → ((𝑧‘dom 𝑇) = 2o → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
5453expr 457 . . . . . . . . . . 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 3164 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o) → (∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) → ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
5756impcom 408 . . . . . . . 8 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 2o)) → ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
5857anassrs 468 . . . . . . 7 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
59 dmeq 5859 . . . . . . . . . 10 (𝑝 = 𝑈 → dom 𝑝 = dom 𝑈)
6059eleq2d 2823 . . . . . . . . 9 (𝑝 = 𝑈 → (dom 𝑇 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑈))
61 breq1 5108 . . . . . . . . . . . 12 (𝑝 = 𝑈 → (𝑝 <s 𝑧𝑈 <s 𝑧))
6261notbid 317 . . . . . . . . . . 11 (𝑝 = 𝑈 → (¬ 𝑝 <s 𝑧 ↔ ¬ 𝑈 <s 𝑧))
63 reseq1 5931 . . . . . . . . . . . 12 (𝑝 = 𝑈 → (𝑝 ↾ suc dom 𝑇) = (𝑈 ↾ suc dom 𝑇))
6463eqeq1d 2738 . . . . . . . . . . 11 (𝑝 = 𝑈 → ((𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇) ↔ (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
6562, 64imbi12d 344 . . . . . . . . . 10 (𝑝 = 𝑈 → ((¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)) ↔ (¬ 𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
6665ralbidv 3174 . . . . . . . . 9 (𝑝 = 𝑈 → (∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)) ↔ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
6760, 66anbi12d 631 . . . . . . . 8 (𝑝 = 𝑈 → ((dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))) ↔ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
6867rspcev 3581 . . . . . . 7 ((𝑈𝐵 ∧ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑈 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))) → ∃𝑝𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
6910, 19, 58, 68syl12anc 835 . . . . . 6 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → ∃𝑝𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
70 nodmon 26998 . . . . . . . . 9 (𝑇 No → dom 𝑇 ∈ On)
714, 70syl 17 . . . . . . . 8 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → dom 𝑇 ∈ On)
7271adantr 481 . . . . . . 7 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 ∈ On)
73 eleq1 2825 . . . . . . . . . 10 (𝑎 = dom 𝑇 → (𝑎 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑝))
74 suceq 6383 . . . . . . . . . . . . . 14 (𝑎 = dom 𝑇 → suc 𝑎 = suc dom 𝑇)
7574reseq2d 5937 . . . . . . . . . . . . 13 (𝑎 = dom 𝑇 → (𝑝 ↾ suc 𝑎) = (𝑝 ↾ suc dom 𝑇))
7674reseq2d 5937 . . . . . . . . . . . . 13 (𝑎 = dom 𝑇 → (𝑧 ↾ suc 𝑎) = (𝑧 ↾ suc dom 𝑇))
7775, 76eqeq12d 2752 . . . . . . . . . . . 12 (𝑎 = dom 𝑇 → ((𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎) ↔ (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))
7877imbi2d 340 . . . . . . . . . . 11 (𝑎 = dom 𝑇 → ((¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ (¬ 𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
7978ralbidv 3174 . . . . . . . . . 10 (𝑎 = dom 𝑇 → (∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇))))
8073, 79anbi12d 631 . . . . . . . . 9 (𝑎 = dom 𝑇 → ((𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
8180rexbidv 3175 . . . . . . . 8 (𝑎 = dom 𝑇 → (∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ ∃𝑝𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc dom 𝑇) = (𝑧 ↾ suc dom 𝑇)))))
8281elabg 3628 . . . . . . 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 256 . . . . 5 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 ∈ {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
851noinfdm 27067 . . . . . . . . 9 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
86853ad2ant1 1133 . . . . . . . 8 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → dom 𝑇 = {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
8786adantl 482 . . . . . . 7 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → dom 𝑇 = {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
8887adantr 481 . . . . . 6 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 = {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
8988eleq2d 2823 . . . . 5 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → (dom 𝑇 ∈ dom 𝑇 ↔ dom 𝑇 ∈ {𝑎 ∣ ∃𝑝𝐵 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐵𝑝 <s 𝑧 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))}))
9084, 89mpbird 256 . . . 4 (((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) ∧ (𝑈‘dom 𝑇) = 2o) → dom 𝑇 ∈ dom 𝑇)
918, 90mtand 814 . . 3 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑈‘dom 𝑇) = 2o)
9291neqned 2950 . 2 ((∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2o)
93 rexanali 3105 . . 3 (∃𝑧𝐵𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2o) ↔ ¬ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o))
94 simpr1 1194 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
95 simpr2 1195 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝐵 No 𝐵𝑉))
96 simplll 773 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧𝐵)
97 simpr3 1196 . . . . . . . . . . . 12 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))
98 simpll 765 . . . . . . . . . . . 12 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧))
9994, 95, 97, 98, 37syl112anc 1374 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧 ↾ dom 𝑇) = 𝑇)
1001noinfbnd1lem4 27074 . . . . . . . . . . 11 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑧𝐵 ∧ (𝑧 ↾ dom 𝑇) = 𝑇)) → (𝑧‘dom 𝑇) ≠ ∅)
10194, 95, 96, 99, 100syl112anc 1374 . . . . . . . . . 10 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧‘dom 𝑇) ≠ ∅)
102101neneqd 2948 . . . . . . . . 9 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = ∅)
103102pm2.21d 121 . . . . . . . 8 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ → (𝑈‘dom 𝑇) ≠ 2o))
1041noinfbnd1lem3 27073 . . . . . . . . . . 11 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑧𝐵 ∧ (𝑧 ↾ dom 𝑇) = 𝑇)) → (𝑧‘dom 𝑇) ≠ 1o)
10594, 95, 96, 99, 104syl112anc 1374 . . . . . . . . . 10 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑧‘dom 𝑇) ≠ 1o)
106105neneqd 2948 . . . . . . . . 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 767 . . . . . . . . 9 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ¬ (𝑧‘dom 𝑇) = 2o)
109 simpr2l 1232 . . . . . . . . . . 11 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝐵 No )
110109, 96sseldd 3945 . . . . . . . . . 10 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → 𝑧 No )
111 nofv 27005 . . . . . . . . . 10 (𝑧 No → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1o ∨ (𝑧‘dom 𝑇) = 2o))
112110, 111syl 17 . . . . . . . . 9 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → ((𝑧‘dom 𝑇) = ∅ ∨ (𝑧‘dom 𝑇) = 1o ∨ (𝑧‘dom 𝑇) = 2o))
113 3orel3 1486 . . . . . . . . 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 858 . . . . . . 7 ((((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2o)
116115ex 413 . . . . . 6 (((𝑧𝐵 ∧ ¬ 𝑈 <s 𝑧) ∧ ¬ (𝑧‘dom 𝑇) = 2o) → ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2o))
117116anasss 467 . . . . 5 ((𝑧𝐵 ∧ (¬ 𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2o)) → ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2o))
118117rexlimiva 3144 . . . 4 (∃𝑧𝐵𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2o) → ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2o))
119118imp 407 . . 3 ((∃𝑧𝐵𝑈 <s 𝑧 ∧ ¬ (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2o)
12093, 119sylanbr 582 . 2 ((¬ ∀𝑧𝐵𝑈 <s 𝑧 → (𝑧‘dom 𝑇) = 2o) ∧ (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇))) → (𝑈‘dom 𝑇) ≠ 2o)
12192, 120pm2.61ian 810 1 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 2o)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3o 1086  w3a 1087   = wceq 1541  wcel 2106  {cab 2713  wne 2943  wral 3064  wrex 3073  cun 3908  wss 3910  c0 4282  ifcif 4486  {csn 4586  cop 4592   class class class wbr 5105  cmpt 5188  dom cdm 5633  cres 5635  Ord word 6316  Oncon0 6317  suc csuc 6319  cio 6446  Fun wfun 6490  cfv 6496  crio 7312  1oc1o 8405  2oc2o 8406   No csur 26988   <s cslt 26989
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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-ord 6320  df-on 6321  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-1o 8412  df-2o 8413  df-no 26991  df-slt 26992  df-bday 26993
This theorem is referenced by:  noinfbnd1lem6  27076
  Copyright terms: Public domain W3C validator