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

Theorem nosupbnd1lem4 31982
 Description: Lemma for nosupbnd1 31985. If 𝑈 is a prolongment of 𝑆 and in 𝐴, then (𝑈‘dom 𝑆) is not undefined. (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
nosupbnd1lem4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ ∅)
Distinct variable groups:   𝐴,𝑔,𝑢,𝑣,𝑥,𝑦   𝑢,𝑈   𝑣,𝑢,𝑥,𝑦
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑈(𝑥,𝑦,𝑣,𝑔)

Proof of Theorem nosupbnd1lem4
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 simpl1 1084 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
2 simpl2 1085 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝐴 No 𝐴 ∈ V))
3 simprl 809 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → 𝑤𝐴)
4 simpl3 1086 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))
5 simprr 811 . . . . . . . . . . 11 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → 𝑈 <s 𝑤)
6 simp2l 1107 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → 𝐴 No )
7 simp3l 1109 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → 𝑈𝐴)
86, 7sseldd 3637 . . . . . . . . . . . 12 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → 𝑈 No )
9 simpl2l 1134 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → 𝐴 No )
109, 3sseldd 3637 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → 𝑤 No )
11 sltso 31952 . . . . . . . . . . . . 13 <s Or No
12 soasym 31783 . . . . . . . . . . . . 13 (( <s Or No ∧ (𝑈 No 𝑤 No )) → (𝑈 <s 𝑤 → ¬ 𝑤 <s 𝑈))
1311, 12mpan 706 . . . . . . . . . . . 12 ((𝑈 No 𝑤 No ) → (𝑈 <s 𝑤 → ¬ 𝑤 <s 𝑈))
148, 10, 13syl2an2r 893 . . . . . . . . . . 11 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑈 <s 𝑤 → ¬ 𝑤 <s 𝑈))
155, 14mpd 15 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → ¬ 𝑤 <s 𝑈)
163, 15jca 553 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑤𝐴 ∧ ¬ 𝑤 <s 𝑈))
17 nosupbnd1.1 . . . . . . . . . 10 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
1817nosupbnd1lem2 31980 . . . . . . . . 9 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ ((𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑤𝐴 ∧ ¬ 𝑤 <s 𝑈))) → (𝑤 ↾ dom 𝑆) = 𝑆)
191, 2, 4, 16, 18syl112anc 1370 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑤 ↾ dom 𝑆) = 𝑆)
2017nosupbnd1lem3 31981 . . . . . . . 8 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑤𝐴 ∧ (𝑤 ↾ dom 𝑆) = 𝑆)) → (𝑤‘dom 𝑆) ≠ 2𝑜)
211, 2, 3, 19, 20syl112anc 1370 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑤‘dom 𝑆) ≠ 2𝑜)
2221neneqd 2828 . . . . . 6 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑤𝐴𝑈 <s 𝑤)) → ¬ (𝑤‘dom 𝑆) = 2𝑜)
2322expr 642 . . . . 5 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ 𝑤𝐴) → (𝑈 <s 𝑤 → ¬ (𝑤‘dom 𝑆) = 2𝑜))
24 imnan 437 . . . . 5 ((𝑈 <s 𝑤 → ¬ (𝑤‘dom 𝑆) = 2𝑜) ↔ ¬ (𝑈 <s 𝑤 ∧ (𝑤‘dom 𝑆) = 2𝑜))
2523, 24sylib 208 . . . 4 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ 𝑤𝐴) → ¬ (𝑈 <s 𝑤 ∧ (𝑤‘dom 𝑆) = 2𝑜))
2625nrexdv 3030 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → ¬ ∃𝑤𝐴 (𝑈 <s 𝑤 ∧ (𝑤‘dom 𝑆) = 2𝑜))
27 simpl3l 1136 . . . . 5 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) → 𝑈𝐴)
28 simpl1 1084 . . . . . 6 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
29 breq2 4689 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝑢 <s 𝑤𝑢 <s 𝑦))
3029cbvrexv 3202 . . . . . . . . 9 (∃𝑤𝐴 𝑢 <s 𝑤 ↔ ∃𝑦𝐴 𝑢 <s 𝑦)
31 breq1 4688 . . . . . . . . . 10 (𝑢 = 𝑥 → (𝑢 <s 𝑦𝑥 <s 𝑦))
3231rexbidv 3081 . . . . . . . . 9 (𝑢 = 𝑥 → (∃𝑦𝐴 𝑢 <s 𝑦 ↔ ∃𝑦𝐴 𝑥 <s 𝑦))
3330, 32syl5bb 272 . . . . . . . 8 (𝑢 = 𝑥 → (∃𝑤𝐴 𝑢 <s 𝑤 ↔ ∃𝑦𝐴 𝑥 <s 𝑦))
3433cbvralv 3201 . . . . . . 7 (∀𝑢𝐴𝑤𝐴 𝑢 <s 𝑤 ↔ ∀𝑥𝐴𝑦𝐴 𝑥 <s 𝑦)
35 dfrex2 3025 . . . . . . . 8 (∃𝑦𝐴 𝑥 <s 𝑦 ↔ ¬ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦)
3635ralbii 3009 . . . . . . 7 (∀𝑥𝐴𝑦𝐴 𝑥 <s 𝑦 ↔ ∀𝑥𝐴 ¬ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦)
37 ralnex 3021 . . . . . . 7 (∀𝑥𝐴 ¬ ∀𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
3834, 36, 373bitri 286 . . . . . 6 (∀𝑢𝐴𝑤𝐴 𝑢 <s 𝑤 ↔ ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
3928, 38sylibr 224 . . . . 5 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) → ∀𝑢𝐴𝑤𝐴 𝑢 <s 𝑤)
40 breq1 4688 . . . . . . 7 (𝑢 = 𝑈 → (𝑢 <s 𝑤𝑈 <s 𝑤))
4140rexbidv 3081 . . . . . 6 (𝑢 = 𝑈 → (∃𝑤𝐴 𝑢 <s 𝑤 ↔ ∃𝑤𝐴 𝑈 <s 𝑤))
4241rspcv 3336 . . . . 5 (𝑈𝐴 → (∀𝑢𝐴𝑤𝐴 𝑢 <s 𝑤 → ∃𝑤𝐴 𝑈 <s 𝑤))
4327, 39, 42sylc 65 . . . 4 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) → ∃𝑤𝐴 𝑈 <s 𝑤)
44 simpl2l 1134 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) → 𝐴 No )
4544, 27sseldd 3637 . . . . . . . . 9 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) → 𝑈 No )
4645adantr 480 . . . . . . . 8 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → 𝑈 No )
4744adantr 480 . . . . . . . . 9 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → 𝐴 No )
48 simprl 809 . . . . . . . . 9 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → 𝑤𝐴)
4947, 48sseldd 3637 . . . . . . . 8 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → 𝑤 No )
5017nosupno 31974 . . . . . . . . . . . 12 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
51503ad2ant2 1103 . . . . . . . . . . 11 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → 𝑆 No )
5251adantr 480 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) → 𝑆 No )
5352adantr 480 . . . . . . . . 9 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → 𝑆 No )
54 nodmon 31928 . . . . . . . . 9 (𝑆 No → dom 𝑆 ∈ On)
5553, 54syl 17 . . . . . . . 8 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → dom 𝑆 ∈ On)
56 simpl3r 1137 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) → (𝑈 ↾ dom 𝑆) = 𝑆)
5756adantr 480 . . . . . . . . 9 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑈 ↾ dom 𝑆) = 𝑆)
58 simpll1 1120 . . . . . . . . . 10 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
59 simpll2 1121 . . . . . . . . . 10 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝐴 No 𝐴 ∈ V))
60 simpll3 1122 . . . . . . . . . 10 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))
61 simprr 811 . . . . . . . . . . . 12 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → 𝑈 <s 𝑤)
6245, 49, 13syl2an2r 893 . . . . . . . . . . . 12 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑈 <s 𝑤 → ¬ 𝑤 <s 𝑈))
6361, 62mpd 15 . . . . . . . . . . 11 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → ¬ 𝑤 <s 𝑈)
6448, 63jca 553 . . . . . . . . . 10 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑤𝐴 ∧ ¬ 𝑤 <s 𝑈))
6558, 59, 60, 64, 18syl112anc 1370 . . . . . . . . 9 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑤 ↾ dom 𝑆) = 𝑆)
6657, 65eqtr4d 2688 . . . . . . . 8 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑈 ↾ dom 𝑆) = (𝑤 ↾ dom 𝑆))
67 simplr 807 . . . . . . . 8 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑈‘dom 𝑆) = ∅)
68 nolt02o 31970 . . . . . . . 8 (((𝑈 No 𝑤 No ∧ dom 𝑆 ∈ On) ∧ ((𝑈 ↾ dom 𝑆) = (𝑤 ↾ dom 𝑆) ∧ 𝑈 <s 𝑤) ∧ (𝑈‘dom 𝑆) = ∅) → (𝑤‘dom 𝑆) = 2𝑜)
6946, 49, 55, 66, 61, 67, 68syl321anc 1388 . . . . . . 7 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ (𝑤𝐴𝑈 <s 𝑤)) → (𝑤‘dom 𝑆) = 2𝑜)
7069expr 642 . . . . . 6 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ 𝑤𝐴) → (𝑈 <s 𝑤 → (𝑤‘dom 𝑆) = 2𝑜))
7170ancld 575 . . . . 5 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) ∧ 𝑤𝐴) → (𝑈 <s 𝑤 → (𝑈 <s 𝑤 ∧ (𝑤‘dom 𝑆) = 2𝑜)))
7271reximdva 3046 . . . 4 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) → (∃𝑤𝐴 𝑈 <s 𝑤 → ∃𝑤𝐴 (𝑈 <s 𝑤 ∧ (𝑤‘dom 𝑆) = 2𝑜)))
7343, 72mpd 15 . . 3 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = ∅) → ∃𝑤𝐴 (𝑈 <s 𝑤 ∧ (𝑤‘dom 𝑆) = 2𝑜))
7426, 73mtand 692 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → ¬ (𝑈‘dom 𝑆) = ∅)
7574neqned 2830 1 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ ∅)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ 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   Or wor 5063  dom cdm 5143   ↾ cres 5145  Oncon0 5761  suc csuc 5763  ℩cio 5887  ‘cfv 5926  ℩crio 6650  2𝑜c2o 7599   No csur 31918
 Copyright terms: Public domain W3C validator