MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nosupno Structured version   Visualization version   GIF version

Theorem nosupno 27763
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 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ 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 3499 . 2 (𝐴𝑉𝐴 ∈ V)
2 nosupno.1 . . 3 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
3 iftrue 4537 . . . . . 6 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
43adantr 480 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
5 simprl 771 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → 𝐴 No )
6 simpl 482 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
7 nomaxmo 27758 . . . . . . . . . 10 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
87ad2antrl 728 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
9 reu5 3380 . . . . . . . . 9 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
106, 8, 9sylanbrc 583 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
11 riotacl 7405 . . . . . . . 8 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
1210, 11syl 17 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
135, 12sseldd 3996 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
14 2on 8519 . . . . . . . . 9 2o ∈ On
1514elexi 3501 . . . . . . . 8 2o ∈ V
1615prid2 4768 . . . . . . 7 2o ∈ {1o, 2o}
1716noextend 27726 . . . . . 6 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )
1813, 17syl 17 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )
194, 18eqeltrd 2839 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) ∈ No )
20 iffalse 4540 . . . . . 6 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ 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 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
22 funmpt 6606 . . . . . . 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 6536 . . . . . . . . 9 (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) ∈ V
25 eqid 2735 . . . . . . . . 9 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
2624, 25dmmpti 6713 . . . . . . . 8 dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
27 ssel2 3990 . . . . . . . . . . . . . . . . 17 ((𝐴 No 𝑢𝐴) → 𝑢 No )
28 nodmon 27710 . . . . . . . . . . . . . . . . 17 (𝑢 No → dom 𝑢 ∈ On)
2927, 28syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 No 𝑢𝐴) → dom 𝑢 ∈ On)
30 onss 7804 . . . . . . . . . . . . . . . 16 (dom 𝑢 ∈ On → dom 𝑢 ⊆ On)
3129, 30syl 17 . . . . . . . . . . . . . . 15 ((𝐴 No 𝑢𝐴) → dom 𝑢 ⊆ On)
3231sseld 3994 . . . . . . . . . . . . . 14 ((𝐴 No 𝑢𝐴) → (𝑦 ∈ dom 𝑢𝑦 ∈ On))
3332adantrd 491 . . . . . . . . . . . . 13 ((𝐴 No 𝑢𝐴) → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ On))
3433rexlimdva 3153 . . . . . . . . . . . 12 (𝐴 No → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ On))
3534abssdv 4078 . . . . . . . . . . 11 (𝐴 No → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ On)
36 simplr 769 . . . . . . . . . . . . . . . . . . 19 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → 𝑎𝑏)
3729adantlr 715 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → dom 𝑢 ∈ On)
38 ontr1 6432 . . . . . . . . . . . . . . . . . . . 20 (dom 𝑢 ∈ On → ((𝑎𝑏𝑏 ∈ dom 𝑢) → 𝑎 ∈ dom 𝑢))
3937, 38syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → ((𝑎𝑏𝑏 ∈ dom 𝑢) → 𝑎 ∈ dom 𝑢))
4036, 39mpand 695 . . . . . . . . . . . . . . . . . 18 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → (𝑏 ∈ dom 𝑢𝑎 ∈ dom 𝑢))
4140adantrd 491 . . . . . . . . . . . . . . . . 17 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → 𝑎 ∈ dom 𝑢))
42 reseq1 5994 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏) → ((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎))
43 onelon 6411 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((dom 𝑢 ∈ On ∧ 𝑏 ∈ dom 𝑢) → 𝑏 ∈ On)
4437, 43sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → 𝑏 ∈ On)
45 onsuc 7831 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 ∈ On → suc 𝑏 ∈ On)
4644, 45syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑏 ∈ On)
47 simpllr 776 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → 𝑎𝑏)
48 eloni 6396 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ On → Ord 𝑏)
4944, 48syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → Ord 𝑏)
50 ordsucelsuc 7842 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Ord 𝑏 → (𝑎𝑏 ↔ suc 𝑎 ∈ suc 𝑏))
5149, 50syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → (𝑎𝑏 ↔ suc 𝑎 ∈ suc 𝑏))
5247, 51mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑎 ∈ suc 𝑏)
53 onelss 6428 . . . . . . . . . . . . . . . . . . . . . . . 24 (suc 𝑏 ∈ On → (suc 𝑎 ∈ suc 𝑏 → suc 𝑎 ⊆ suc 𝑏))
5446, 52, 53sylc 65 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑎 ⊆ suc 𝑏)
5554resabs1d 6028 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = (𝑢 ↾ suc 𝑎))
5654resabs1d 6028 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))
5755, 56eqeq12d 2751 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → (((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎) ↔ (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
5842, 57imbitrid 244 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏) → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
5958imim2d 57 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)) → (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
6059ralimdv 3167 . . . . . . . . . . . . . . . . . 18 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)) → ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
6160expimpd 453 . . . . . . . . . . . . . . . . 17 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
6241, 61jcad 512 . . . . . . . . . . . . . . . 16 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
6362reximdva 3166 . . . . . . . . . . . . . . 15 ((𝐴 No 𝑎𝑏) → (∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → ∃𝑢𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
6463expimpd 453 . . . . . . . . . . . . . 14 (𝐴 No → ((𝑎𝑏 ∧ ∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))) → ∃𝑢𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
65 vex 3482 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
66 eleq1w 2822 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 → (𝑦 ∈ dom 𝑢𝑏 ∈ dom 𝑢))
67 suceq 6452 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑏 → suc 𝑦 = suc 𝑏)
6867reseq2d 6000 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑏 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑏))
6967reseq2d 6000 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑏 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑏))
7068, 69eqeq12d 2751 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑏 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))
7170imbi2d 340 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
7271ralbidv 3176 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
7366, 72anbi12d 632 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑏 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
7473rexbidv 3177 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑏 → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
7565, 74elab 3681 . . . . . . . . . . . . . . 15 (𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
7675anbi2i 623 . . . . . . . . . . . . . 14 ((𝑎𝑏𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) ↔ (𝑎𝑏 ∧ ∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
77 vex 3482 . . . . . . . . . . . . . . 15 𝑎 ∈ V
78 eleq1w 2822 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑎 → (𝑦 ∈ dom 𝑢𝑎 ∈ dom 𝑢))
79 suceq 6452 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑎 → suc 𝑦 = suc 𝑎)
8079reseq2d 6000 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑎 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑎))
8179reseq2d 6000 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑎 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑎))
8280, 81eqeq12d 2751 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑎 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
8382imbi2d 340 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑎 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
8483ralbidv 3176 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑎 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
8578, 84anbi12d 632 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑎 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
8685rexbidv 3177 . . . . . . . . . . . . . . 15 (𝑦 = 𝑎 → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
8777, 86elab 3681 . . . . . . . . . . . . . 14 (𝑎 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
8864, 76, 873imtr4g 296 . . . . . . . . . . . . 13 (𝐴 No → ((𝑎𝑏𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
8988alrimivv 1926 . . . . . . . . . . . 12 (𝐴 No → ∀𝑎𝑏((𝑎𝑏𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
90 dftr2 5267 . . . . . . . . . . . 12 (Tr {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∀𝑎𝑏((𝑎𝑏𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
9189, 90sylibr 234 . . . . . . . . . . 11 (𝐴 No → Tr {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
92 dford5 7803 . . . . . . . . . . 11 (Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ({𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ On ∧ Tr {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
9335, 91, 92sylanbrc 583 . . . . . . . . . 10 (𝐴 No → Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
9493adantr 480 . . . . . . . . 9 ((𝐴 No 𝐴 ∈ V) → Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
95 bdayfo 27737 . . . . . . . . . . . . . . 15 bday : No onto→On
96 fofun 6822 . . . . . . . . . . . . . . 15 ( bday : No onto→On → Fun bday )
9795, 96ax-mp 5 . . . . . . . . . . . . . 14 Fun bday
98 funimaexg 6654 . . . . . . . . . . . . . 14 ((Fun bday 𝐴 ∈ V) → ( bday 𝐴) ∈ V)
9997, 98mpan 690 . . . . . . . . . . . . 13 (𝐴 ∈ V → ( bday 𝐴) ∈ V)
10099uniexd 7761 . . . . . . . . . . . 12 (𝐴 ∈ V → ( bday 𝐴) ∈ V)
101100adantl 481 . . . . . . . . . . 11 ((𝐴 No 𝐴 ∈ V) → ( bday 𝐴) ∈ V)
102 simpl 482 . . . . . . . . . . . . . 14 ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ dom 𝑢)
103102reximi 3082 . . . . . . . . . . . . 13 (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → ∃𝑢𝐴 𝑦 ∈ dom 𝑢)
104103ss2abi 4077 . . . . . . . . . . . 12 {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ {𝑦 ∣ ∃𝑢𝐴 𝑦 ∈ dom 𝑢}
105 bdayval 27708 . . . . . . . . . . . . . . . . . . 19 (𝑢 No → ( bday 𝑢) = dom 𝑢)
10627, 105syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐴 No 𝑢𝐴) → ( bday 𝑢) = dom 𝑢)
107 fofn 6823 . . . . . . . . . . . . . . . . . . . 20 ( bday : No onto→On → bday Fn No )
10895, 107ax-mp 5 . . . . . . . . . . . . . . . . . . 19 bday Fn No
109 fnfvima 7253 . . . . . . . . . . . . . . . . . . 19 (( bday Fn No 𝐴 No 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
110108, 109mp3an1 1447 . . . . . . . . . . . . . . . . . 18 ((𝐴 No 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
111106, 110eqeltrrd 2840 . . . . . . . . . . . . . . . . 17 ((𝐴 No 𝑢𝐴) → dom 𝑢 ∈ ( bday 𝐴))
112 elssuni 4942 . . . . . . . . . . . . . . . . 17 (dom 𝑢 ∈ ( bday 𝐴) → dom 𝑢 ( bday 𝐴))
113111, 112syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 No 𝑢𝐴) → dom 𝑢 ( bday 𝐴))
114113sseld 3994 . . . . . . . . . . . . . . 15 ((𝐴 No 𝑢𝐴) → (𝑦 ∈ dom 𝑢𝑦 ( bday 𝐴)))
115114rexlimdva 3153 . . . . . . . . . . . . . 14 (𝐴 No → (∃𝑢𝐴 𝑦 ∈ dom 𝑢𝑦 ( bday 𝐴)))
116115abssdv 4078 . . . . . . . . . . . . 13 (𝐴 No → {𝑦 ∣ ∃𝑢𝐴 𝑦 ∈ dom 𝑢} ⊆ ( bday 𝐴))
117116adantr 480 . . . . . . . . . . . 12 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 𝑦 ∈ dom 𝑢} ⊆ ( bday 𝐴))
118104, 117sstrid 4007 . . . . . . . . . . 11 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ ( bday 𝐴))
119101, 118ssexd 5330 . . . . . . . . . 10 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ V)
120 elong 6394 . . . . . . . . . 10 ({𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ V → ({𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On ↔ Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
121119, 120syl 17 . . . . . . . . 9 ((𝐴 No 𝐴 ∈ V) → ({𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On ↔ Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
12294, 121mpbird 257 . . . . . . . 8 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On)
12326, 122eqeltrid 2843 . . . . . . 7 ((𝐴 No 𝐴 ∈ V) → dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ∈ On)
124123adantl 481 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ∈ On)
12525rnmpt 5971 . . . . . . . 8 ran (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑧 ∣ ∃𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))}
126 vex 3482 . . . . . . . . . . . 12 𝑔 ∈ V
127 eleq1w 2822 . . . . . . . . . . . . . 14 (𝑦 = 𝑔 → (𝑦 ∈ dom 𝑢𝑔 ∈ dom 𝑢))
128 suceq 6452 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑔 → suc 𝑦 = suc 𝑔)
129128reseq2d 6000 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑔 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑔))
130128reseq2d 6000 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑔 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑔))
131129, 130eqeq12d 2751 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑔 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
132131imbi2d 340 . . . . . . . . . . . . . . 15 (𝑦 = 𝑔 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
133132ralbidv 3176 . . . . . . . . . . . . . 14 (𝑦 = 𝑔 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
134127, 133anbi12d 632 . . . . . . . . . . . . 13 (𝑦 = 𝑔 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))))
135134rexbidv 3177 . . . . . . . . . . . 12 (𝑦 = 𝑔 → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))))
136126, 135elab 3681 . . . . . . . . . . 11 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
137 eqid 2735 . . . . . . . . . . . . . . . . . . 19 (𝑢𝑔) = (𝑢𝑔)
138 fvex 6920 . . . . . . . . . . . . . . . . . . . 20 (𝑢𝑔) ∈ V
139 eqeq2 2747 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑢𝑔) → ((𝑢𝑔) = 𝑥 ↔ (𝑢𝑔) = (𝑢𝑔)))
1401393anbi3d 1441 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑢𝑔) → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = (𝑢𝑔))))
141138, 140spcev 3606 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = (𝑢𝑔)) → ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
142137, 141mp3an3 1449 . . . . . . . . . . . . . . . . . 18 ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
143142reximi 3082 . . . . . . . . . . . . . . . . 17 (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑢𝐴𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
144 rexcom4 3286 . . . . . . . . . . . . . . . . 17 (∃𝑢𝐴𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ ∃𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
145143, 144sylib 218 . . . . . . . . . . . . . . . 16 (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
146145adantl 481 . . . . . . . . . . . . . . 15 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
147 nosupprefixmo 27760 . . . . . . . . . . . . . . . 16 (𝐴 No → ∃*𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
148147adantr 480 . . . . . . . . . . . . . . 15 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃*𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
149 df-eu 2567 . . . . . . . . . . . . . . 15 (∃!𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ (∃𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ∧ ∃*𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
150146, 148, 149sylanbrc 583 . . . . . . . . . . . . . 14 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃!𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
151 vex 3482 . . . . . . . . . . . . . . 15 𝑧 ∈ V
152 eqeq2 2747 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → ((𝑢𝑔) = 𝑥 ↔ (𝑢𝑔) = 𝑧))
1531523anbi3d 1441 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧)))
154153rexbidv 3177 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧)))
155154iota2 6552 . . . . . . . . . . . . . . 15 ((𝑧 ∈ V ∧ ∃!𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) ↔ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) = 𝑧))
156151, 155mpan 690 . . . . . . . . . . . . . 14 (∃!𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) ↔ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) = 𝑧))
157150, 156syl 17 . . . . . . . . . . . . 13 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) ↔ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) = 𝑧))
158 eqcom 2742 . . . . . . . . . . . . 13 ((℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) = 𝑧𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
159157, 158bitrdi 287 . . . . . . . . . . . 12 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) ↔ 𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
160 simprr3 1222 . . . . . . . . . . . . . . 15 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → (𝑢𝑔) = 𝑧)
16127adantrr 717 . . . . . . . . . . . . . . . . 17 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → 𝑢 No )
162 norn 27711 . . . . . . . . . . . . . . . . 17 (𝑢 No → ran 𝑢 ⊆ {1o, 2o})
163161, 162syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → ran 𝑢 ⊆ {1o, 2o})
164 nofun 27709 . . . . . . . . . . . . . . . . . 18 (𝑢 No → Fun 𝑢)
165161, 164syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → Fun 𝑢)
166 simprr1 1220 . . . . . . . . . . . . . . . . 17 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → 𝑔 ∈ dom 𝑢)
167 fvelrn 7096 . . . . . . . . . . . . . . . . 17 ((Fun 𝑢𝑔 ∈ dom 𝑢) → (𝑢𝑔) ∈ ran 𝑢)
168165, 166, 167syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → (𝑢𝑔) ∈ ran 𝑢)
169163, 168sseldd 3996 . . . . . . . . . . . . . . 15 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → (𝑢𝑔) ∈ {1o, 2o})
170160, 169eqeltrrd 2840 . . . . . . . . . . . . . 14 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → 𝑧 ∈ {1o, 2o})
171170rexlimdvaa 3154 . . . . . . . . . . . . 13 (𝐴 No → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) → 𝑧 ∈ {1o, 2o}))
172171adantr 480 . . . . . . . . . . . 12 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) → 𝑧 ∈ {1o, 2o}))
173159, 172sylbird 260 . . . . . . . . . . 11 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) → 𝑧 ∈ {1o, 2o}))
174136, 173sylan2b 594 . . . . . . . . . 10 ((𝐴 No 𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → (𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) → 𝑧 ∈ {1o, 2o}))
175174rexlimdva 3153 . . . . . . . . 9 (𝐴 No → (∃𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) → 𝑧 ∈ {1o, 2o}))
176175abssdv 4078 . . . . . . . 8 (𝐴 No → {𝑧 ∣ ∃𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))} ⊆ {1o, 2o})
177125, 176eqsstrid 4044 . . . . . . 7 (𝐴 No → ran (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ⊆ {1o, 2o})
178177ad2antrl 728 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ran (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ⊆ {1o, 2o})
179 elno2 27714 . . . . . 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 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ⊆ {1o, 2o}))
18023, 124, 178, 179syl3anbrc 1342 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ∈ No )
18121, 180eqeltrd 2839 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) ∈ No )
18219, 181pm2.61ian 812 . . 3 ((𝐴 No 𝐴 ∈ V) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) ∈ No )
1832, 182eqeltrid 2843 . 2 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
1841, 183sylan2 593 1 ((𝐴 No 𝐴𝑉) → 𝑆 No )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086  wal 1535   = wceq 1537  wex 1776  wcel 2106  ∃*wmo 2536  ∃!weu 2566  {cab 2712  wral 3059  wrex 3068  ∃!wreu 3376  ∃*wrmo 3377  Vcvv 3478  cun 3961  wss 3963  ifcif 4531  {csn 4631  {cpr 4633  cop 4637   cuni 4912   class class class wbr 5148  cmpt 5231  Tr wtr 5265  dom cdm 5689  ran crn 5690  cres 5691  cima 5692  Ord word 6385  Oncon0 6386  suc csuc 6388  cio 6514  Fun wfun 6557   Fn wfn 6558  ontowfo 6561  cfv 6563  crio 7387  1oc1o 8498  2oc2o 8499   No csur 27699   <s cslt 27700   bday cbday 27701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ord 6389  df-on 6390  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fo 6569  df-fv 6571  df-riota 7388  df-1o 8505  df-2o 8506  df-no 27702  df-slt 27703  df-bday 27704
This theorem is referenced by:  nosupbday  27765  nosupres  27767  nosupbnd1lem1  27768  nosupbnd1lem2  27769  nosupbnd1lem3  27770  nosupbnd1lem4  27771  nosupbnd1lem5  27772  nosupbnd1lem6  27773  nosupbnd2  27776  nosupinfsep  27792  noetasuplem1  27793  noetasuplem2  27794  noetasuplem3  27795  noetasuplem4  27796  noetalem1  27801
  Copyright terms: Public domain W3C validator