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
 Copyright terms: Public domain W3C validator