Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nosupbnd1lem5 Structured version   Visualization version   GIF version

Theorem nosupbnd1lem5 31983
Description: Lemma for nosupbnd1 31985. If 𝑈 is a prolongment of 𝑆 and in 𝐴, then (𝑈‘dom 𝑆) is not 1𝑜. (Contributed by Scott Fenton, 6-Dec-2021.)
Hypothesis
Ref Expression
nosupbnd1.1 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
nosupbnd1lem5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ 1𝑜)
Distinct variable group:   𝐴,𝑔,𝑢,𝑣,𝑥,𝑦
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑈(𝑥,𝑦,𝑣,𝑢,𝑔)

Proof of Theorem nosupbnd1lem5
Dummy variables 𝑎 𝑝 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nosupbnd1.1 . . . . . . . 8 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
21nosupno 31974 . . . . . . 7 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
323ad2ant2 1103 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → 𝑆 No )
43adantl 481 . . . . 5 ((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) → 𝑆 No )
5 nodmord 31931 . . . . 5 (𝑆 No → Ord dom 𝑆)
6 ordirr 5779 . . . . 5 (Ord dom 𝑆 → ¬ dom 𝑆 ∈ dom 𝑆)
74, 5, 63syl 18 . . . 4 ((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) → ¬ dom 𝑆 ∈ dom 𝑆)
8 simpr3l 1142 . . . . . . 7 ((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) → 𝑈𝐴)
98adantr 480 . . . . . 6 (((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) ∧ (𝑈‘dom 𝑆) = 1𝑜) → 𝑈𝐴)
10 ndmfv 6256 . . . . . . . . 9 (¬ dom 𝑆 ∈ dom 𝑈 → (𝑈‘dom 𝑆) = ∅)
11 1on 7612 . . . . . . . . . . . . . 14 1𝑜 ∈ On
1211elexi 3244 . . . . . . . . . . . . 13 1𝑜 ∈ V
1312prid1 4329 . . . . . . . . . . . 12 1𝑜 ∈ {1𝑜, 2𝑜}
1413nosgnn0i 31937 . . . . . . . . . . 11 ∅ ≠ 1𝑜
15 neeq1 2885 . . . . . . . . . . 11 ((𝑈‘dom 𝑆) = ∅ → ((𝑈‘dom 𝑆) ≠ 1𝑜 ↔ ∅ ≠ 1𝑜))
1614, 15mpbiri 248 . . . . . . . . . 10 ((𝑈‘dom 𝑆) = ∅ → (𝑈‘dom 𝑆) ≠ 1𝑜)
1716neneqd 2828 . . . . . . . . 9 ((𝑈‘dom 𝑆) = ∅ → ¬ (𝑈‘dom 𝑆) = 1𝑜)
1810, 17syl 17 . . . . . . . 8 (¬ dom 𝑆 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑆) = 1𝑜)
1918con4i 113 . . . . . . 7 ((𝑈‘dom 𝑆) = 1𝑜 → dom 𝑆 ∈ dom 𝑈)
2019adantl 481 . . . . . 6 (((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) ∧ (𝑈‘dom 𝑆) = 1𝑜) → dom 𝑆 ∈ dom 𝑈)
21 simp2l 1107 . . . . . . . . . . . . . . . . 17 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → 𝐴 No )
22 simp3l 1109 . . . . . . . . . . . . . . . . 17 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → 𝑈𝐴)
2321, 22sseldd 3637 . . . . . . . . . . . . . . . 16 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → 𝑈 No )
2423adantr 480 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) → 𝑈 No )
2524adantr 480 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → 𝑈 No )
26 nofun 31927 . . . . . . . . . . . . . 14 (𝑈 No → Fun 𝑈)
2725, 26syl 17 . . . . . . . . . . . . 13 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → Fun 𝑈)
28 simpl2l 1134 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) → 𝐴 No )
29 simpll 805 . . . . . . . . . . . . . . 15 (((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜) → 𝑧𝐴)
30 ssel2 3631 . . . . . . . . . . . . . . 15 ((𝐴 No 𝑧𝐴) → 𝑧 No )
3128, 29, 30syl2an 493 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → 𝑧 No )
32 nofun 31927 . . . . . . . . . . . . . 14 (𝑧 No → Fun 𝑧)
3331, 32syl 17 . . . . . . . . . . . . 13 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → Fun 𝑧)
34 simpl3r 1137 . . . . . . . . . . . . . . 15 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) → (𝑈 ↾ dom 𝑆) = 𝑆)
3534adantr 480 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → (𝑈 ↾ dom 𝑆) = 𝑆)
36 simpll1 1120 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
37 simpll2 1121 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → (𝐴 No 𝐴 ∈ V))
38 simpll3 1122 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))
39 simprl 809 . . . . . . . . . . . . . . 15 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈))
401nosupbnd1lem2 31980 . . . . . . . . . . . . . . 15 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ ((𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈))) → (𝑧 ↾ dom 𝑆) = 𝑆)
4136, 37, 38, 39, 40syl112anc 1370 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → (𝑧 ↾ dom 𝑆) = 𝑆)
4235, 41eqtr4d 2688 . . . . . . . . . . . . 13 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → (𝑈 ↾ dom 𝑆) = (𝑧 ↾ dom 𝑆))
4319adantl 481 . . . . . . . . . . . . . 14 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) → dom 𝑆 ∈ dom 𝑈)
4443adantr 480 . . . . . . . . . . . . 13 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → dom 𝑆 ∈ dom 𝑈)
45 ndmfv 6256 . . . . . . . . . . . . . . . . 17 (¬ dom 𝑆 ∈ dom 𝑧 → (𝑧‘dom 𝑆) = ∅)
46 neeq1 2885 . . . . . . . . . . . . . . . . . . 19 ((𝑧‘dom 𝑆) = ∅ → ((𝑧‘dom 𝑆) ≠ 1𝑜 ↔ ∅ ≠ 1𝑜))
4714, 46mpbiri 248 . . . . . . . . . . . . . . . . . 18 ((𝑧‘dom 𝑆) = ∅ → (𝑧‘dom 𝑆) ≠ 1𝑜)
4847neneqd 2828 . . . . . . . . . . . . . . . . 17 ((𝑧‘dom 𝑆) = ∅ → ¬ (𝑧‘dom 𝑆) = 1𝑜)
4945, 48syl 17 . . . . . . . . . . . . . . . 16 (¬ dom 𝑆 ∈ dom 𝑧 → ¬ (𝑧‘dom 𝑆) = 1𝑜)
5049con4i 113 . . . . . . . . . . . . . . 15 ((𝑧‘dom 𝑆) = 1𝑜 → dom 𝑆 ∈ dom 𝑧)
5150adantl 481 . . . . . . . . . . . . . 14 (((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜) → dom 𝑆 ∈ dom 𝑧)
5251adantl 481 . . . . . . . . . . . . 13 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → dom 𝑆 ∈ dom 𝑧)
53 simplr 807 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → (𝑈‘dom 𝑆) = 1𝑜)
54 simprr 811 . . . . . . . . . . . . . 14 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → (𝑧‘dom 𝑆) = 1𝑜)
5553, 54eqtr4d 2688 . . . . . . . . . . . . 13 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → (𝑈‘dom 𝑆) = (𝑧‘dom 𝑆))
56 eqfunressuc 31786 . . . . . . . . . . . . 13 (((Fun 𝑈 ∧ Fun 𝑧) ∧ (𝑈 ↾ dom 𝑆) = (𝑧 ↾ dom 𝑆) ∧ (dom 𝑆 ∈ dom 𝑈 ∧ dom 𝑆 ∈ dom 𝑧 ∧ (𝑈‘dom 𝑆) = (𝑧‘dom 𝑆))) → (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆))
5727, 33, 42, 44, 52, 55, 56syl213anc 1385 . . . . . . . . . . . 12 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ (𝑧‘dom 𝑆) = 1𝑜)) → (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆))
5857expr 642 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → ((𝑧‘dom 𝑆) = 1𝑜 → (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)))
5958expr 642 . . . . . . . . . 10 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ 𝑧𝐴) → (¬ 𝑧 <s 𝑈 → ((𝑧‘dom 𝑆) = 1𝑜 → (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆))))
6059a2d 29 . . . . . . . . 9 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) ∧ 𝑧𝐴) → ((¬ 𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) → (¬ 𝑧 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆))))
6160ralimdva 2991 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜) → (∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) → ∀𝑧𝐴𝑧 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆))))
6261impcom 445 . . . . . . 7 ((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 1𝑜)) → ∀𝑧𝐴𝑧 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)))
6362anassrs 681 . . . . . 6 (((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) ∧ (𝑈‘dom 𝑆) = 1𝑜) → ∀𝑧𝐴𝑧 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)))
64 dmeq 5356 . . . . . . . . 9 (𝑝 = 𝑈 → dom 𝑝 = dom 𝑈)
6564eleq2d 2716 . . . . . . . 8 (𝑝 = 𝑈 → (dom 𝑆 ∈ dom 𝑝 ↔ dom 𝑆 ∈ dom 𝑈))
66 breq2 4689 . . . . . . . . . . 11 (𝑝 = 𝑈 → (𝑧 <s 𝑝𝑧 <s 𝑈))
6766notbid 307 . . . . . . . . . 10 (𝑝 = 𝑈 → (¬ 𝑧 <s 𝑝 ↔ ¬ 𝑧 <s 𝑈))
68 reseq1 5422 . . . . . . . . . . 11 (𝑝 = 𝑈 → (𝑝 ↾ suc dom 𝑆) = (𝑈 ↾ suc dom 𝑆))
6968eqeq1d 2653 . . . . . . . . . 10 (𝑝 = 𝑈 → ((𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆) ↔ (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)))
7067, 69imbi12d 333 . . . . . . . . 9 (𝑝 = 𝑈 → ((¬ 𝑧 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)) ↔ (¬ 𝑧 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆))))
7170ralbidv 3015 . . . . . . . 8 (𝑝 = 𝑈 → (∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)) ↔ ∀𝑧𝐴𝑧 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆))))
7265, 71anbi12d 747 . . . . . . 7 (𝑝 = 𝑈 → ((dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆))) ↔ (dom 𝑆 ∈ dom 𝑈 ∧ ∀𝑧𝐴𝑧 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)))))
7372rspcev 3340 . . . . . 6 ((𝑈𝐴 ∧ (dom 𝑆 ∈ dom 𝑈 ∧ ∀𝑧𝐴𝑧 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)))) → ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆))))
749, 20, 63, 73syl12anc 1364 . . . . 5 (((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) ∧ (𝑈‘dom 𝑆) = 1𝑜) → ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆))))
75 simplr1 1123 . . . . . . 7 (((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) ∧ (𝑈‘dom 𝑆) = 1𝑜) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
761nosupdm 31975 . . . . . . . 8 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑎 ∣ ∃𝑝𝐴 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))})
7776eleq2d 2716 . . . . . . 7 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (dom 𝑆 ∈ dom 𝑆 ↔ dom 𝑆 ∈ {𝑎 ∣ ∃𝑝𝐴 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))}))
7875, 77syl 17 . . . . . 6 (((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) ∧ (𝑈‘dom 𝑆) = 1𝑜) → (dom 𝑆 ∈ dom 𝑆 ↔ dom 𝑆 ∈ {𝑎 ∣ ∃𝑝𝐴 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))}))
794adantr 480 . . . . . . 7 (((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) ∧ (𝑈‘dom 𝑆) = 1𝑜) → 𝑆 No )
80 nodmon 31928 . . . . . . 7 (𝑆 No → dom 𝑆 ∈ On)
81 eleq1 2718 . . . . . . . . . 10 (𝑎 = dom 𝑆 → (𝑎 ∈ dom 𝑝 ↔ dom 𝑆 ∈ dom 𝑝))
82 suceq 5828 . . . . . . . . . . . . . 14 (𝑎 = dom 𝑆 → suc 𝑎 = suc dom 𝑆)
8382reseq2d 5428 . . . . . . . . . . . . 13 (𝑎 = dom 𝑆 → (𝑝 ↾ suc 𝑎) = (𝑝 ↾ suc dom 𝑆))
8482reseq2d 5428 . . . . . . . . . . . . 13 (𝑎 = dom 𝑆 → (𝑧 ↾ suc 𝑎) = (𝑧 ↾ suc dom 𝑆))
8583, 84eqeq12d 2666 . . . . . . . . . . . 12 (𝑎 = dom 𝑆 → ((𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎) ↔ (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)))
8685imbi2d 329 . . . . . . . . . . 11 (𝑎 = dom 𝑆 → ((¬ 𝑧 <s 𝑝 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ (¬ 𝑧 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆))))
8786ralbidv 3015 . . . . . . . . . 10 (𝑎 = dom 𝑆 → (∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)) ↔ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆))))
8881, 87anbi12d 747 . . . . . . . . 9 (𝑎 = dom 𝑆 → ((𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)))))
8988rexbidv 3081 . . . . . . . 8 (𝑎 = dom 𝑆 → (∃𝑝𝐴 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎))) ↔ ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)))))
9089elabg 3383 . . . . . . 7 (dom 𝑆 ∈ On → (dom 𝑆 ∈ {𝑎 ∣ ∃𝑝𝐴 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))} ↔ ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)))))
9179, 80, 903syl 18 . . . . . 6 (((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) ∧ (𝑈‘dom 𝑆) = 1𝑜) → (dom 𝑆 ∈ {𝑎 ∣ ∃𝑝𝐴 (𝑎 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc 𝑎) = (𝑧 ↾ suc 𝑎)))} ↔ ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)))))
9278, 91bitrd 268 . . . . 5 (((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) ∧ (𝑈‘dom 𝑆) = 1𝑜) → (dom 𝑆 ∈ dom 𝑆 ↔ ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑧𝐴𝑧 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑧 ↾ suc dom 𝑆)))))
9374, 92mpbird 247 . . . 4 (((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) ∧ (𝑈‘dom 𝑆) = 1𝑜) → dom 𝑆 ∈ dom 𝑆)
947, 93mtand 692 . . 3 ((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) → ¬ (𝑈‘dom 𝑆) = 1𝑜)
9594neqned 2830 . 2 ((∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) → (𝑈‘dom 𝑆) ≠ 1𝑜)
96 rexanali 3027 . . 3 (∃𝑧𝐴𝑧 <s 𝑈 ∧ ¬ (𝑧‘dom 𝑆) = 1𝑜) ↔ ¬ ∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜))
97 simpl 472 . . . . . . . . . . 11 ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) → 𝑧𝐴)
9821, 97, 30syl2an 493 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → 𝑧 No )
99 nofv 31935 . . . . . . . . . 10 (𝑧 No → ((𝑧‘dom 𝑆) = ∅ ∨ (𝑧‘dom 𝑆) = 1𝑜 ∨ (𝑧‘dom 𝑆) = 2𝑜))
10098, 99syl 17 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → ((𝑧‘dom 𝑆) = ∅ ∨ (𝑧‘dom 𝑆) = 1𝑜 ∨ (𝑧‘dom 𝑆) = 2𝑜))
101 3orel2 31718 . . . . . . . . 9 (¬ (𝑧‘dom 𝑆) = 1𝑜 → (((𝑧‘dom 𝑆) = ∅ ∨ (𝑧‘dom 𝑆) = 1𝑜 ∨ (𝑧‘dom 𝑆) = 2𝑜) → ((𝑧‘dom 𝑆) = ∅ ∨ (𝑧‘dom 𝑆) = 2𝑜)))
102100, 101syl5com 31 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → (¬ (𝑧‘dom 𝑆) = 1𝑜 → ((𝑧‘dom 𝑆) = ∅ ∨ (𝑧‘dom 𝑆) = 2𝑜)))
103102imdistanda 729 . . . . . . 7 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ ¬ (𝑧‘dom 𝑆) = 1𝑜) → ((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ ((𝑧‘dom 𝑆) = ∅ ∨ (𝑧‘dom 𝑆) = 2𝑜))))
104 simpl1 1084 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
105 simpl2 1085 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → (𝐴 No 𝐴 ∈ V))
106 simprl 809 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → 𝑧𝐴)
107 simpl3 1086 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))
108 simpr 476 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈))
109104, 105, 107, 108, 40syl112anc 1370 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → (𝑧 ↾ dom 𝑆) = 𝑆)
1101nosupbnd1lem4 31982 . . . . . . . . . . . 12 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑧𝐴 ∧ (𝑧 ↾ dom 𝑆) = 𝑆)) → (𝑧‘dom 𝑆) ≠ ∅)
111104, 105, 106, 109, 110syl112anc 1370 . . . . . . . . . . 11 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → (𝑧‘dom 𝑆) ≠ ∅)
112111neneqd 2828 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → ¬ (𝑧‘dom 𝑆) = ∅)
113112pm2.21d 118 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → ((𝑧‘dom 𝑆) = ∅ → (𝑈‘dom 𝑆) ≠ 1𝑜))
1141nosupbnd1lem3 31981 . . . . . . . . . . . 12 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑧𝐴 ∧ (𝑧 ↾ dom 𝑆) = 𝑆)) → (𝑧‘dom 𝑆) ≠ 2𝑜)
115104, 105, 106, 109, 114syl112anc 1370 . . . . . . . . . . 11 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → (𝑧‘dom 𝑆) ≠ 2𝑜)
116115neneqd 2828 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → ¬ (𝑧‘dom 𝑆) = 2𝑜)
117116pm2.21d 118 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → ((𝑧‘dom 𝑆) = 2𝑜 → (𝑈‘dom 𝑆) ≠ 1𝑜))
118113, 117jaod 394 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈)) → (((𝑧‘dom 𝑆) = ∅ ∨ (𝑧‘dom 𝑆) = 2𝑜) → (𝑈‘dom 𝑆) ≠ 1𝑜))
119118expimpd 628 . . . . . . 7 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ ((𝑧‘dom 𝑆) = ∅ ∨ (𝑧‘dom 𝑆) = 2𝑜)) → (𝑈‘dom 𝑆) ≠ 1𝑜))
120103, 119syldc 48 . . . . . 6 (((𝑧𝐴 ∧ ¬ 𝑧 <s 𝑈) ∧ ¬ (𝑧‘dom 𝑆) = 1𝑜) → ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ 1𝑜))
121120anasss 680 . . . . 5 ((𝑧𝐴 ∧ (¬ 𝑧 <s 𝑈 ∧ ¬ (𝑧‘dom 𝑆) = 1𝑜)) → ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ 1𝑜))
122121rexlimiva 3057 . . . 4 (∃𝑧𝐴𝑧 <s 𝑈 ∧ ¬ (𝑧‘dom 𝑆) = 1𝑜) → ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ 1𝑜))
123122imp 444 . . 3 ((∃𝑧𝐴𝑧 <s 𝑈 ∧ ¬ (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) → (𝑈‘dom 𝑆) ≠ 1𝑜)
12496, 123sylanbr 489 . 2 ((¬ ∀𝑧𝐴𝑧 <s 𝑈 → (𝑧‘dom 𝑆) = 1𝑜) ∧ (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))) → (𝑈‘dom 𝑆) ≠ 1𝑜)
12595, 124pm2.61ian 848 1 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ 1𝑜)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3o 1053  w3a 1054   = wceq 1523  wcel 2030  {cab 2637  wne 2823  wral 2941  wrex 2942  Vcvv 3231  cun 3605  wss 3607  c0 3948  ifcif 4119  {csn 4210  cop 4216   class class class wbr 4685  cmpt 4762  dom cdm 5143  cres 5145  Ord word 5760  Oncon0 5761  suc csuc 5763  cio 5887  Fun wfun 5920  cfv 5926  crio 6650  1𝑜c1o 7598  2𝑜c2o 7599   No csur 31918   <s cslt 31919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-ord 5764  df-on 5765  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-1o 7605  df-2o 7606  df-no 31921  df-slt 31922  df-bday 31923
This theorem is referenced by:  nosupbnd1lem6  31984
  Copyright terms: Public domain W3C validator