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

Theorem nosupno 31974
 Description: The next several theorems deal with a surreal "supremum". This surreal will ultimately be shown to bound 𝐴 below and bound the restriction of any surreal above. We begin by showing that the given expression actually defines a surreal number. (Contributed by Scott Fenton, 5-Dec-2021.)
Hypothesis
Ref Expression
nosupno.1 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
nosupno ((𝐴 No 𝐴𝑉) → 𝑆 No )
Distinct variable group:   𝑥,𝐴,𝑦,𝑔,𝑣,𝑢
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑉(𝑥,𝑦,𝑣,𝑢,𝑔)

Proof of Theorem nosupno
Dummy variables 𝑎 𝑏 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3243 . 2 (𝐴𝑉𝐴 ∈ V)
2 nosupno.1 . . 3 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
3 iftrue 4125 . . . . . 6 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}))
43adantr 480 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}))
5 simprl 809 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → 𝐴 No )
6 simpl 472 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
7 nomaxmo 31972 . . . . . . . . . 10 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
87ad2antrl 764 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
9 reu5 3189 . . . . . . . . 9 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
106, 8, 9sylanbrc 699 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
11 riotacl 6665 . . . . . . . 8 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
1210, 11syl 17 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
135, 12sseldd 3637 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
14 2on 7613 . . . . . . . . 9 2𝑜 ∈ On
1514elexi 3244 . . . . . . . 8 2𝑜 ∈ V
1615prid2 4330 . . . . . . 7 2𝑜 ∈ {1𝑜, 2𝑜}
1716noextend 31944 . . . . . 6 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}) ∈ No )
1813, 17syl 17 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}) ∈ No )
194, 18eqeltrd 2730 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) ∈ No )
20 iffalse 4128 . . . . . 6 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
2120adantr 480 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
22 funmpt 5964 . . . . . . 7 Fun (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
2322a1i 11 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → Fun (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
24 iotaex 5906 . . . . . . . . 9 (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) ∈ V
25 eqid 2651 . . . . . . . . 9 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
2624, 25dmmpti 6061 . . . . . . . 8 dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
27 ssel2 3631 . . . . . . . . . . . . . . . . 17 ((𝐴 No 𝑢𝐴) → 𝑢 No )
28 nodmon 31928 . . . . . . . . . . . . . . . . 17 (𝑢 No → dom 𝑢 ∈ On)
2927, 28syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 No 𝑢𝐴) → dom 𝑢 ∈ On)
30 onss 7032 . . . . . . . . . . . . . . . 16 (dom 𝑢 ∈ On → dom 𝑢 ⊆ On)
3129, 30syl 17 . . . . . . . . . . . . . . 15 ((𝐴 No 𝑢𝐴) → dom 𝑢 ⊆ On)
3231sseld 3635 . . . . . . . . . . . . . 14 ((𝐴 No 𝑢𝐴) → (𝑦 ∈ dom 𝑢𝑦 ∈ On))
3332adantrd 483 . . . . . . . . . . . . 13 ((𝐴 No 𝑢𝐴) → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ On))
3433rexlimdva 3060 . . . . . . . . . . . 12 (𝐴 No → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ On))
3534abssdv 3709 . . . . . . . . . . 11 (𝐴 No → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ On)
36 simplr 807 . . . . . . . . . . . . . . . . . . 19 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → 𝑎𝑏)
3729adantlr 751 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → dom 𝑢 ∈ On)
38 ontr1 5809 . . . . . . . . . . . . . . . . . . . 20 (dom 𝑢 ∈ On → ((𝑎𝑏𝑏 ∈ dom 𝑢) → 𝑎 ∈ dom 𝑢))
3937, 38syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → ((𝑎𝑏𝑏 ∈ dom 𝑢) → 𝑎 ∈ dom 𝑢))
4036, 39mpand 711 . . . . . . . . . . . . . . . . . 18 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → (𝑏 ∈ dom 𝑢𝑎 ∈ dom 𝑢))
4140adantrd 483 . . . . . . . . . . . . . . . . 17 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → 𝑎 ∈ dom 𝑢))
42 reseq1 5422 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏) → ((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎))
43 onelon 5786 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((dom 𝑢 ∈ On ∧ 𝑏 ∈ dom 𝑢) → 𝑏 ∈ On)
4437, 43sylan 487 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → 𝑏 ∈ On)
45 suceloni 7055 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 ∈ On → suc 𝑏 ∈ On)
4644, 45syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑏 ∈ On)
47 simpllr 815 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → 𝑎𝑏)
48 eloni 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ On → Ord 𝑏)
4944, 48syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → Ord 𝑏)
50 ordsucelsuc 7064 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Ord 𝑏 → (𝑎𝑏 ↔ suc 𝑎 ∈ suc 𝑏))
5149, 50syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → (𝑎𝑏 ↔ suc 𝑎 ∈ suc 𝑏))
5247, 51mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑎 ∈ suc 𝑏)
53 onelss 5804 . . . . . . . . . . . . . . . . . . . . . . . 24 (suc 𝑏 ∈ On → (suc 𝑎 ∈ suc 𝑏 → suc 𝑎 ⊆ suc 𝑏))
5446, 52, 53sylc 65 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑎 ⊆ suc 𝑏)
5554resabs1d 5463 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = (𝑢 ↾ suc 𝑎))
5654resabs1d 5463 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))
5755, 56eqeq12d 2666 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → (((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎) ↔ (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
5842, 57syl5ib 234 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏) → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
5958imim2d 57 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)) → (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
6059ralimdv 2992 . . . . . . . . . . . . . . . . . 18 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)) → ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
6160expimpd 628 . . . . . . . . . . . . . . . . 17 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
6241, 61jcad 554 . . . . . . . . . . . . . . . 16 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
6362reximdva 3046 . . . . . . . . . . . . . . 15 ((𝐴 No 𝑎𝑏) → (∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → ∃𝑢𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
6463expimpd 628 . . . . . . . . . . . . . 14 (𝐴 No → ((𝑎𝑏 ∧ ∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))) → ∃𝑢𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
65 vex 3234 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
66 eleq1 2718 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 → (𝑦 ∈ dom 𝑢𝑏 ∈ dom 𝑢))
67 suceq 5828 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑏 → suc 𝑦 = suc 𝑏)
6867reseq2d 5428 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑏 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑏))
6967reseq2d 5428 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑏 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑏))
7068, 69eqeq12d 2666 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑏 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))
7170imbi2d 329 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
7271ralbidv 3015 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
7366, 72anbi12d 747 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑏 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
7473rexbidv 3081 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑏 → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
7565, 74elab 3382 . . . . . . . . . . . . . . 15 (𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
7675anbi2i 730 . . . . . . . . . . . . . 14 ((𝑎𝑏𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) ↔ (𝑎𝑏 ∧ ∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
77 vex 3234 . . . . . . . . . . . . . . 15 𝑎 ∈ V
78 eleq1 2718 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑎 → (𝑦 ∈ dom 𝑢𝑎 ∈ dom 𝑢))
79 suceq 5828 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑎 → suc 𝑦 = suc 𝑎)
8079reseq2d 5428 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑎 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑎))
8179reseq2d 5428 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑎 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑎))
8280, 81eqeq12d 2666 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑎 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
8382imbi2d 329 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑎 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
8483ralbidv 3015 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑎 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
8578, 84anbi12d 747 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑎 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
8685rexbidv 3081 . . . . . . . . . . . . . . 15 (𝑦 = 𝑎 → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
8777, 86elab 3382 . . . . . . . . . . . . . 14 (𝑎 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
8864, 76, 873imtr4g 285 . . . . . . . . . . . . 13 (𝐴 No → ((𝑎𝑏𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
8988alrimivv 1896 . . . . . . . . . . . 12 (𝐴 No → ∀𝑎𝑏((𝑎𝑏𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
90 dftr2 4787 . . . . . . . . . . . 12 (Tr {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∀𝑎𝑏((𝑎𝑏𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
9189, 90sylibr 224 . . . . . . . . . . 11 (𝐴 No → Tr {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
92 dford5 31734 . . . . . . . . . . 11 (Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ({𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ On ∧ Tr {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
9335, 91, 92sylanbrc 699 . . . . . . . . . 10 (𝐴 No → Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
9493adantr 480 . . . . . . . . 9 ((𝐴 No 𝐴 ∈ V) → Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
95 bdayfo 31953 . . . . . . . . . . . . . . 15 bday : No onto→On
96 fofun 6154 . . . . . . . . . . . . . . 15 ( bday : No onto→On → Fun bday )
9795, 96ax-mp 5 . . . . . . . . . . . . . 14 Fun bday
98 funimaexg 6013 . . . . . . . . . . . . . 14 ((Fun bday 𝐴 ∈ V) → ( bday 𝐴) ∈ V)
9997, 98mpan 706 . . . . . . . . . . . . 13 (𝐴 ∈ V → ( bday 𝐴) ∈ V)
100 uniexg 6997 . . . . . . . . . . . . 13 (( bday 𝐴) ∈ V → ( bday 𝐴) ∈ V)
10199, 100syl 17 . . . . . . . . . . . 12 (𝐴 ∈ V → ( bday 𝐴) ∈ V)
102101adantl 481 . . . . . . . . . . 11 ((𝐴 No 𝐴 ∈ V) → ( bday 𝐴) ∈ V)
103 simpl 472 . . . . . . . . . . . . . 14 ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ dom 𝑢)
104103reximi 3040 . . . . . . . . . . . . 13 (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → ∃𝑢𝐴 𝑦 ∈ dom 𝑢)
105104ss2abi 3707 . . . . . . . . . . . 12 {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ {𝑦 ∣ ∃𝑢𝐴 𝑦 ∈ dom 𝑢}
106 bdayval 31926 . . . . . . . . . . . . . . . . . . 19 (𝑢 No → ( bday 𝑢) = dom 𝑢)
10727, 106syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐴 No 𝑢𝐴) → ( bday 𝑢) = dom 𝑢)
108 fofn 6155 . . . . . . . . . . . . . . . . . . . 20 ( bday : No onto→On → bday Fn No )
10995, 108ax-mp 5 . . . . . . . . . . . . . . . . . . 19 bday Fn No
110 fnfvima 6536 . . . . . . . . . . . . . . . . . . 19 (( bday Fn No 𝐴 No 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
111109, 110mp3an1 1451 . . . . . . . . . . . . . . . . . 18 ((𝐴 No 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
112107, 111eqeltrrd 2731 . . . . . . . . . . . . . . . . 17 ((𝐴 No 𝑢𝐴) → dom 𝑢 ∈ ( bday 𝐴))
113 elssuni 4499 . . . . . . . . . . . . . . . . 17 (dom 𝑢 ∈ ( bday 𝐴) → dom 𝑢 ( bday 𝐴))
114112, 113syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 No 𝑢𝐴) → dom 𝑢 ( bday 𝐴))
115114sseld 3635 . . . . . . . . . . . . . . 15 ((𝐴 No 𝑢𝐴) → (𝑦 ∈ dom 𝑢𝑦 ( bday 𝐴)))
116115rexlimdva 3060 . . . . . . . . . . . . . 14 (𝐴 No → (∃𝑢𝐴 𝑦 ∈ dom 𝑢𝑦 ( bday 𝐴)))
117116abssdv 3709 . . . . . . . . . . . . 13 (𝐴 No → {𝑦 ∣ ∃𝑢𝐴 𝑦 ∈ dom 𝑢} ⊆ ( bday 𝐴))
118117adantr 480 . . . . . . . . . . . 12 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 𝑦 ∈ dom 𝑢} ⊆ ( bday 𝐴))
119105, 118syl5ss 3647 . . . . . . . . . . 11 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ ( bday 𝐴))
120102, 119ssexd 4838 . . . . . . . . . 10 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ V)
121 elong 5769 . . . . . . . . . 10 ({𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ V → ({𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On ↔ Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
122120, 121syl 17 . . . . . . . . 9 ((𝐴 No 𝐴 ∈ V) → ({𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On ↔ Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
12394, 122mpbird 247 . . . . . . . 8 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On)
12426, 123syl5eqel 2734 . . . . . . 7 ((𝐴 No 𝐴 ∈ V) → dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ∈ On)
125124adantl 481 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ∈ On)
12625rnmpt 5403 . . . . . . . 8 ran (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑧 ∣ ∃𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))}
127 vex 3234 . . . . . . . . . . . 12 𝑔 ∈ V
128 eleq1 2718 . . . . . . . . . . . . . 14 (𝑦 = 𝑔 → (𝑦 ∈ dom 𝑢𝑔 ∈ dom 𝑢))
129 suceq 5828 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑔 → suc 𝑦 = suc 𝑔)
130129reseq2d 5428 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑔 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑔))
131129reseq2d 5428 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑔 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑔))
132130, 131eqeq12d 2666 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑔 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
133132imbi2d 329 . . . . . . . . . . . . . . 15 (𝑦 = 𝑔 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
134133ralbidv 3015 . . . . . . . . . . . . . 14 (𝑦 = 𝑔 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
135128, 134anbi12d 747 . . . . . . . . . . . . 13 (𝑦 = 𝑔 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))))
136135rexbidv 3081 . . . . . . . . . . . 12 (𝑦 = 𝑔 → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))))
137127, 136elab 3382 . . . . . . . . . . 11 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
138 eqid 2651 . . . . . . . . . . . . . . . . . . 19 (𝑢𝑔) = (𝑢𝑔)
139 fvex 6239 . . . . . . . . . . . . . . . . . . . 20 (𝑢𝑔) ∈ V
140 eqeq2 2662 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑢𝑔) → ((𝑢𝑔) = 𝑥 ↔ (𝑢𝑔) = (𝑢𝑔)))
1411403anbi3d 1445 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑢𝑔) → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = (𝑢𝑔))))
142139, 141spcev 3331 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = (𝑢𝑔)) → ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
143138, 142mp3an3 1453 . . . . . . . . . . . . . . . . . 18 ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
144143reximi 3040 . . . . . . . . . . . . . . . . 17 (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑢𝐴𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
145 rexcom4 3256 . . . . . . . . . . . . . . . . 17 (∃𝑢𝐴𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ ∃𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
146144, 145sylib 208 . . . . . . . . . . . . . . . 16 (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
147146adantl 481 . . . . . . . . . . . . . . 15 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
148 noprefixmo 31973 . . . . . . . . . . . . . . . 16 (𝐴 No → ∃*𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
149148adantr 480 . . . . . . . . . . . . . . 15 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃*𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
150 eu5 2524 . . . . . . . . . . . . . . 15 (∃!𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ (∃𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ∧ ∃*𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
151147, 149, 150sylanbrc 699 . . . . . . . . . . . . . 14 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃!𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
152 vex 3234 . . . . . . . . . . . . . . 15 𝑧 ∈ V
153 eqeq2 2662 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → ((𝑢𝑔) = 𝑥 ↔ (𝑢𝑔) = 𝑧))
1541533anbi3d 1445 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧)))
155154rexbidv 3081 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧)))
156155iota2 5915 . . . . . . . . . . . . . . 15 ((𝑧 ∈ V ∧ ∃!𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) ↔ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) = 𝑧))
157152, 156mpan 706 . . . . . . . . . . . . . 14 (∃!𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) ↔ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) = 𝑧))
158151, 157syl 17 . . . . . . . . . . . . 13 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) ↔ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) = 𝑧))
159 eqcom 2658 . . . . . . . . . . . . 13 ((℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) = 𝑧𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
160158, 159syl6bb 276 . . . . . . . . . . . 12 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) ↔ 𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
161 simprr3 1131 . . . . . . . . . . . . . . 15 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → (𝑢𝑔) = 𝑧)
16227adantrr 753 . . . . . . . . . . . . . . . . 17 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → 𝑢 No )
163 norn 31929 . . . . . . . . . . . . . . . . 17 (𝑢 No → ran 𝑢 ⊆ {1𝑜, 2𝑜})
164162, 163syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → ran 𝑢 ⊆ {1𝑜, 2𝑜})
165 nofun 31927 . . . . . . . . . . . . . . . . . 18 (𝑢 No → Fun 𝑢)
166162, 165syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → Fun 𝑢)
167 simprr1 1129 . . . . . . . . . . . . . . . . 17 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → 𝑔 ∈ dom 𝑢)
168 fvelrn 6392 . . . . . . . . . . . . . . . . 17 ((Fun 𝑢𝑔 ∈ dom 𝑢) → (𝑢𝑔) ∈ ran 𝑢)
169166, 167, 168syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → (𝑢𝑔) ∈ ran 𝑢)
170164, 169sseldd 3637 . . . . . . . . . . . . . . 15 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → (𝑢𝑔) ∈ {1𝑜, 2𝑜})
171161, 170eqeltrrd 2731 . . . . . . . . . . . . . 14 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → 𝑧 ∈ {1𝑜, 2𝑜})
172171rexlimdvaa 3061 . . . . . . . . . . . . 13 (𝐴 No → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) → 𝑧 ∈ {1𝑜, 2𝑜}))
173172adantr 480 . . . . . . . . . . . 12 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) → 𝑧 ∈ {1𝑜, 2𝑜}))
174160, 173sylbird 250 . . . . . . . . . . 11 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) → 𝑧 ∈ {1𝑜, 2𝑜}))
175137, 174sylan2b 491 . . . . . . . . . 10 ((𝐴 No 𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → (𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) → 𝑧 ∈ {1𝑜, 2𝑜}))
176175rexlimdva 3060 . . . . . . . . 9 (𝐴 No → (∃𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) → 𝑧 ∈ {1𝑜, 2𝑜}))
177176abssdv 3709 . . . . . . . 8 (𝐴 No → {𝑧 ∣ ∃𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))} ⊆ {1𝑜, 2𝑜})
178126, 177syl5eqss 3682 . . . . . . 7 (𝐴 No → ran (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ⊆ {1𝑜, 2𝑜})
179178ad2antrl 764 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ran (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ⊆ {1𝑜, 2𝑜})
180 elno2 31932 . . . . . 6 ((𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ∈ No ↔ (Fun (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ∧ dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ∈ On ∧ ran (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ⊆ {1𝑜, 2𝑜}))
18123, 125, 179, 180syl3anbrc 1265 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ∈ No )
18221, 181eqeltrd 2730 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) ∈ No )
18319, 182pm2.61ian 848 . . 3 ((𝐴 No 𝐴 ∈ V) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) ∈ No )
1842, 183syl5eqel 2734 . 2 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
1851, 184sylan2 490 1 ((𝐴 No 𝐴𝑉) → 𝑆 No )
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054  ∀wal 1521   = wceq 1523  ∃wex 1744   ∈ wcel 2030  ∃!weu 2498  ∃*wmo 2499  {cab 2637  ∀wral 2941  ∃wrex 2942  ∃!wreu 2943  ∃*wrmo 2944  Vcvv 3231   ∪ cun 3605   ⊆ wss 3607  ifcif 4119  {csn 4210  {cpr 4212  ⟨cop 4216  ∪ cuni 4468   class class class wbr 4685   ↦ cmpt 4762  Tr wtr 4785  dom cdm 5143  ran crn 5144   ↾ cres 5145   “ cima 5146  Ord word 5760  Oncon0 5761  suc csuc 5763  ℩cio 5887  Fun wfun 5920   Fn wfn 5921  –onto→wfo 5924  ‘cfv 5926  ℩crio 6650  1𝑜c1o 7598  2𝑜c2o 7599   No csur 31918
 Copyright terms: Public domain W3C validator