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

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

Proof of Theorem nosupbnd1lem3
Dummy variables 𝑝 𝑞 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nosupbnd1.1 . . . . . 6 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
21nosupno 33352 . . . . 5 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
323ad2ant2 1131 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → 𝑆 No )
4 nodmord 33309 . . . 4 (𝑆 No → Ord dom 𝑆)
5 ordirr 6180 . . . 4 (Ord dom 𝑆 → ¬ dom 𝑆 ∈ dom 𝑆)
63, 4, 53syl 18 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → ¬ dom 𝑆 ∈ dom 𝑆)
7 simpl3l 1225 . . . . 5 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) → 𝑈𝐴)
8 ndmfv 6680 . . . . . . . 8 (¬ dom 𝑆 ∈ dom 𝑈 → (𝑈‘dom 𝑆) = ∅)
9 2on 8101 . . . . . . . . . . . . 13 2o ∈ On
109elexi 3460 . . . . . . . . . . . 12 2o ∈ V
1110prid2 4659 . . . . . . . . . . 11 2o ∈ {1o, 2o}
1211nosgnn0i 33315 . . . . . . . . . 10 ∅ ≠ 2o
13 neeq1 3049 . . . . . . . . . 10 ((𝑈‘dom 𝑆) = ∅ → ((𝑈‘dom 𝑆) ≠ 2o ↔ ∅ ≠ 2o))
1412, 13mpbiri 261 . . . . . . . . 9 ((𝑈‘dom 𝑆) = ∅ → (𝑈‘dom 𝑆) ≠ 2o)
1514neneqd 2992 . . . . . . . 8 ((𝑈‘dom 𝑆) = ∅ → ¬ (𝑈‘dom 𝑆) = 2o)
168, 15syl 17 . . . . . . 7 (¬ dom 𝑆 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑆) = 2o)
1716con4i 114 . . . . . 6 ((𝑈‘dom 𝑆) = 2o → dom 𝑆 ∈ dom 𝑈)
1817adantl 485 . . . . 5 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) → dom 𝑆 ∈ dom 𝑈)
19 simpl2l 1223 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) → 𝐴 No )
2019adantr 484 . . . . . . . . 9 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → 𝐴 No )
217adantr 484 . . . . . . . . 9 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → 𝑈𝐴)
2220, 21sseldd 3916 . . . . . . . 8 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → 𝑈 No )
23 simprl 770 . . . . . . . . 9 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → 𝑞𝐴)
2420, 23sseldd 3916 . . . . . . . 8 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → 𝑞 No )
253adantr 484 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) → 𝑆 No )
2625adantr 484 . . . . . . . . 9 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → 𝑆 No )
27 nodmon 33306 . . . . . . . . 9 (𝑆 No → dom 𝑆 ∈ On)
2826, 27syl 17 . . . . . . . 8 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → dom 𝑆 ∈ On)
29 simpl3r 1226 . . . . . . . . . 10 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) → (𝑈 ↾ dom 𝑆) = 𝑆)
3029adantr 484 . . . . . . . . 9 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → (𝑈 ↾ dom 𝑆) = 𝑆)
31 simpll1 1209 . . . . . . . . . 10 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
32 simpll2 1210 . . . . . . . . . 10 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → (𝐴 No 𝐴 ∈ V))
33 simpll3 1211 . . . . . . . . . 10 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆))
34 simpr 488 . . . . . . . . . 10 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈))
351nosupbnd1lem2 33358 . . . . . . . . . 10 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ ((𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈))) → (𝑞 ↾ dom 𝑆) = 𝑆)
3631, 32, 33, 34, 35syl112anc 1371 . . . . . . . . 9 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → (𝑞 ↾ dom 𝑆) = 𝑆)
3730, 36eqtr4d 2836 . . . . . . . 8 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → (𝑈 ↾ dom 𝑆) = (𝑞 ↾ dom 𝑆))
38 simplr 768 . . . . . . . 8 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → (𝑈‘dom 𝑆) = 2o)
39 simprr 772 . . . . . . . 8 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → ¬ 𝑞 <s 𝑈)
40 nolesgn2ores 33328 . . . . . . . 8 (((𝑈 No 𝑞 No ∧ dom 𝑆 ∈ On) ∧ ((𝑈 ↾ dom 𝑆) = (𝑞 ↾ dom 𝑆) ∧ (𝑈‘dom 𝑆) = 2o) ∧ ¬ 𝑞 <s 𝑈) → (𝑈 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆))
4122, 24, 28, 37, 38, 39, 40syl321anc 1389 . . . . . . 7 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ (𝑞𝐴 ∧ ¬ 𝑞 <s 𝑈)) → (𝑈 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆))
4241expr 460 . . . . . 6 ((((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) ∧ 𝑞𝐴) → (¬ 𝑞 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)))
4342ralrimiva 3149 . . . . 5 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) → ∀𝑞𝐴𝑞 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)))
44 dmeq 5737 . . . . . . . 8 (𝑝 = 𝑈 → dom 𝑝 = dom 𝑈)
4544eleq2d 2875 . . . . . . 7 (𝑝 = 𝑈 → (dom 𝑆 ∈ dom 𝑝 ↔ dom 𝑆 ∈ dom 𝑈))
46 breq2 5035 . . . . . . . . . 10 (𝑝 = 𝑈 → (𝑞 <s 𝑝𝑞 <s 𝑈))
4746notbid 321 . . . . . . . . 9 (𝑝 = 𝑈 → (¬ 𝑞 <s 𝑝 ↔ ¬ 𝑞 <s 𝑈))
48 reseq1 5813 . . . . . . . . . 10 (𝑝 = 𝑈 → (𝑝 ↾ suc dom 𝑆) = (𝑈 ↾ suc dom 𝑆))
4948eqeq1d 2800 . . . . . . . . 9 (𝑝 = 𝑈 → ((𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆) ↔ (𝑈 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)))
5047, 49imbi12d 348 . . . . . . . 8 (𝑝 = 𝑈 → ((¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)) ↔ (¬ 𝑞 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆))))
5150ralbidv 3162 . . . . . . 7 (𝑝 = 𝑈 → (∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)) ↔ ∀𝑞𝐴𝑞 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆))))
5245, 51anbi12d 633 . . . . . 6 (𝑝 = 𝑈 → ((dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆))) ↔ (dom 𝑆 ∈ dom 𝑈 ∧ ∀𝑞𝐴𝑞 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)))))
5352rspcev 3571 . . . . 5 ((𝑈𝐴 ∧ (dom 𝑆 ∈ dom 𝑈 ∧ ∀𝑞𝐴𝑞 <s 𝑈 → (𝑈 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)))) → ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆))))
547, 18, 43, 53syl12anc 835 . . . 4 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) → ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆))))
551nosupdm 33353 . . . . . . . 8 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑧 ∣ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})
5655eleq2d 2875 . . . . . . 7 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (dom 𝑆 ∈ dom 𝑆 ↔ dom 𝑆 ∈ {𝑧 ∣ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))}))
57563ad2ant1 1130 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (dom 𝑆 ∈ dom 𝑆 ↔ dom 𝑆 ∈ {𝑧 ∣ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))}))
58 eleq1 2877 . . . . . . . . . 10 (𝑧 = dom 𝑆 → (𝑧 ∈ dom 𝑝 ↔ dom 𝑆 ∈ dom 𝑝))
59 suceq 6227 . . . . . . . . . . . . . 14 (𝑧 = dom 𝑆 → suc 𝑧 = suc dom 𝑆)
6059reseq2d 5819 . . . . . . . . . . . . 13 (𝑧 = dom 𝑆 → (𝑝 ↾ suc 𝑧) = (𝑝 ↾ suc dom 𝑆))
6159reseq2d 5819 . . . . . . . . . . . . 13 (𝑧 = dom 𝑆 → (𝑞 ↾ suc 𝑧) = (𝑞 ↾ suc dom 𝑆))
6260, 61eqeq12d 2814 . . . . . . . . . . . 12 (𝑧 = dom 𝑆 → ((𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧) ↔ (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)))
6362imbi2d 344 . . . . . . . . . . 11 (𝑧 = dom 𝑆 → ((¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)) ↔ (¬ 𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆))))
6463ralbidv 3162 . . . . . . . . . 10 (𝑧 = dom 𝑆 → (∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)) ↔ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆))))
6558, 64anbi12d 633 . . . . . . . . 9 (𝑧 = dom 𝑆 → ((𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) ↔ (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)))))
6665rexbidv 3256 . . . . . . . 8 (𝑧 = dom 𝑆 → (∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) ↔ ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)))))
6766elabg 3614 . . . . . . 7 (dom 𝑆 ∈ On → (dom 𝑆 ∈ {𝑧 ∣ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} ↔ ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)))))
683, 27, 673syl 18 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (dom 𝑆 ∈ {𝑧 ∣ ∃𝑝𝐴 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} ↔ ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)))))
6957, 68bitrd 282 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (dom 𝑆 ∈ dom 𝑆 ↔ ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)))))
7069adantr 484 . . . 4 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) → (dom 𝑆 ∈ dom 𝑆 ↔ ∃𝑝𝐴 (dom 𝑆 ∈ dom 𝑝 ∧ ∀𝑞𝐴𝑞 <s 𝑝 → (𝑝 ↾ suc dom 𝑆) = (𝑞 ↾ suc dom 𝑆)))))
7154, 70mpbird 260 . . 3 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) ∧ (𝑈‘dom 𝑆) = 2o) → dom 𝑆 ∈ dom 𝑆)
726, 71mtand 815 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → ¬ (𝑈‘dom 𝑆) = 2o)
7372neqned 2994 1 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴 ∧ (𝑈 ↾ dom 𝑆) = 𝑆)) → (𝑈‘dom 𝑆) ≠ 2o)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∪ cun 3879   ⊆ wss 3881  ∅c0 4243  ifcif 4425  {csn 4525  ⟨cop 4531   class class class wbr 5031   ↦ cmpt 5111  dom cdm 5520   ↾ cres 5522  Ord word 6161  Oncon0 6162  suc csuc 6164  ℩cio 6284  ‘cfv 6327  ℩crio 7097  1oc1o 8085  2oc2o 8086   No csur 33296
 Copyright terms: Public domain W3C validator