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

Theorem nosupno 27656
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 3492 . 2 (𝐴𝑉𝐴 ∈ V)
2 nosupno.1 . . 3 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
3 iftrue 4538 . . . . . 6 (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
43adantr 479 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}))
5 simprl 769 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → 𝐴 No )
6 simpl 481 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
7 nomaxmo 27651 . . . . . . . . . 10 (𝐴 No → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
87ad2antrl 726 . . . . . . . . 9 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
9 reu5 3376 . . . . . . . . 9 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦))
106, 8, 9sylanbrc 581 . . . . . . . 8 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
11 riotacl 7400 . . . . . . . 8 (∃!𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
1210, 11syl 17 . . . . . . 7 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴)
135, 12sseldd 3983 . . . . . 6 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No )
14 2on 8507 . . . . . . . . 9 2o ∈ On
1514elexi 3493 . . . . . . . 8 2o ∈ V
1615prid2 4772 . . . . . . 7 2o ∈ {1o, 2o}
1716noextend 27619 . . . . . 6 ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∈ No → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )
1813, 17syl 17 . . . . 5 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}) ∈ No )
194, 18eqeltrd 2829 . . . 4 ((∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) ∈ No )
20 iffalse 4541 . . . . . 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 479 . . . . 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 6596 . . . . . . 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 6526 . . . . . . . . 9 (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) ∈ V
25 eqid 2728 . . . . . . . . 9 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
2624, 25dmmpti 6704 . . . . . . . 8 dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
27 ssel2 3977 . . . . . . . . . . . . . . . . 17 ((𝐴 No 𝑢𝐴) → 𝑢 No )
28 nodmon 27603 . . . . . . . . . . . . . . . . 17 (𝑢 No → dom 𝑢 ∈ On)
2927, 28syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 No 𝑢𝐴) → dom 𝑢 ∈ On)
30 onss 7793 . . . . . . . . . . . . . . . 16 (dom 𝑢 ∈ On → dom 𝑢 ⊆ On)
3129, 30syl 17 . . . . . . . . . . . . . . 15 ((𝐴 No 𝑢𝐴) → dom 𝑢 ⊆ On)
3231sseld 3981 . . . . . . . . . . . . . 14 ((𝐴 No 𝑢𝐴) → (𝑦 ∈ dom 𝑢𝑦 ∈ On))
3332adantrd 490 . . . . . . . . . . . . 13 ((𝐴 No 𝑢𝐴) → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ On))
3433rexlimdva 3152 . . . . . . . . . . . 12 (𝐴 No → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ On))
3534abssdv 4065 . . . . . . . . . . 11 (𝐴 No → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ On)
36 simplr 767 . . . . . . . . . . . . . . . . . . 19 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → 𝑎𝑏)
3729adantlr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → dom 𝑢 ∈ On)
38 ontr1 6420 . . . . . . . . . . . . . . . . . . . 20 (dom 𝑢 ∈ On → ((𝑎𝑏𝑏 ∈ dom 𝑢) → 𝑎 ∈ dom 𝑢))
3937, 38syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → ((𝑎𝑏𝑏 ∈ dom 𝑢) → 𝑎 ∈ dom 𝑢))
4036, 39mpand 693 . . . . . . . . . . . . . . . . . 18 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → (𝑏 ∈ dom 𝑢𝑎 ∈ dom 𝑢))
4140adantrd 490 . . . . . . . . . . . . . . . . 17 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → 𝑎 ∈ dom 𝑢))
42 reseq1 5983 . . . . . . . . . . . . . . . . . . . . 21 ((𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏) → ((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎))
43 onelon 6399 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((dom 𝑢 ∈ On ∧ 𝑏 ∈ dom 𝑢) → 𝑏 ∈ On)
4437, 43sylan 578 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → 𝑏 ∈ On)
45 onsuc 7820 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏 ∈ On → suc 𝑏 ∈ On)
4644, 45syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑏 ∈ On)
47 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → 𝑎𝑏)
48 eloni 6384 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 ∈ On → Ord 𝑏)
4944, 48syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → Ord 𝑏)
50 ordsucelsuc 7831 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (Ord 𝑏 → (𝑎𝑏 ↔ suc 𝑎 ∈ suc 𝑏))
5149, 50syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → (𝑎𝑏 ↔ suc 𝑎 ∈ suc 𝑏))
5247, 51mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑎 ∈ suc 𝑏)
53 onelss 6416 . . . . . . . . . . . . . . . . . . . . . . . 24 (suc 𝑏 ∈ On → (suc 𝑎 ∈ suc 𝑏 → suc 𝑎 ⊆ suc 𝑏))
5446, 52, 53sylc 65 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → suc 𝑎 ⊆ suc 𝑏)
5554resabs1d 6017 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = (𝑢 ↾ suc 𝑎))
5654resabs1d 6017 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))
5755, 56eqeq12d 2744 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → (((𝑢 ↾ suc 𝑏) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝑏) ↾ suc 𝑎) ↔ (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
5842, 57imbitrid 243 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏) → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
5958imim2d 57 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)) → (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
6059ralimdv 3166 . . . . . . . . . . . . . . . . . 18 ((((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) ∧ 𝑏 ∈ dom 𝑢) → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)) → ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
6160expimpd 452 . . . . . . . . . . . . . . . . 17 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
6241, 61jcad 511 . . . . . . . . . . . . . . . 16 (((𝐴 No 𝑎𝑏) ∧ 𝑢𝐴) → ((𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
6362reximdva 3165 . . . . . . . . . . . . . . 15 ((𝐴 No 𝑎𝑏) → (∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))) → ∃𝑢𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
6463expimpd 452 . . . . . . . . . . . . . 14 (𝐴 No → ((𝑎𝑏 ∧ ∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))) → ∃𝑢𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
65 vex 3477 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
66 eleq1w 2812 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 → (𝑦 ∈ dom 𝑢𝑏 ∈ dom 𝑢))
67 suceq 6440 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑏 → suc 𝑦 = suc 𝑏)
6867reseq2d 5989 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑏 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑏))
6967reseq2d 5989 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑏 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑏))
7068, 69eqeq12d 2744 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑏 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))
7170imbi2d 339 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
7271ralbidv 3175 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
7366, 72anbi12d 630 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑏 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
7473rexbidv 3176 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑏 → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
7565, 74elab 3669 . . . . . . . . . . . . . . 15 (𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏))))
7675anbi2i 621 . . . . . . . . . . . . . 14 ((𝑎𝑏𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) ↔ (𝑎𝑏 ∧ ∃𝑢𝐴 (𝑏 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑏) = (𝑣 ↾ suc 𝑏)))))
77 vex 3477 . . . . . . . . . . . . . . 15 𝑎 ∈ V
78 eleq1w 2812 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑎 → (𝑦 ∈ dom 𝑢𝑎 ∈ dom 𝑢))
79 suceq 6440 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑎 → suc 𝑦 = suc 𝑎)
8079reseq2d 5989 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑎 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑎))
8179reseq2d 5989 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑎 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑎))
8280, 81eqeq12d 2744 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑎 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
8382imbi2d 339 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑎 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
8483ralbidv 3175 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑎 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
8578, 84anbi12d 630 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑎 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
8685rexbidv 3176 . . . . . . . . . . . . . . 15 (𝑦 = 𝑎 → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))))
8777, 86elab 3669 . . . . . . . . . . . . . 14 (𝑎 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐴 (𝑎 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
8864, 76, 873imtr4g 295 . . . . . . . . . . . . 13 (𝐴 No → ((𝑎𝑏𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
8988alrimivv 1923 . . . . . . . . . . . 12 (𝐴 No → ∀𝑎𝑏((𝑎𝑏𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
90 dftr2 5271 . . . . . . . . . . . 12 (Tr {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∀𝑎𝑏((𝑎𝑏𝑏 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → 𝑎 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
9189, 90sylibr 233 . . . . . . . . . . 11 (𝐴 No → Tr {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
92 dford5 7792 . . . . . . . . . . 11 (Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ({𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ On ∧ Tr {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}))
9335, 91, 92sylanbrc 581 . . . . . . . . . 10 (𝐴 No → Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
9493adantr 479 . . . . . . . . 9 ((𝐴 No 𝐴 ∈ V) → Ord {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
95 bdayfo 27630 . . . . . . . . . . . . . . 15 bday : No onto→On
96 fofun 6817 . . . . . . . . . . . . . . 15 ( bday : No onto→On → Fun bday )
9795, 96ax-mp 5 . . . . . . . . . . . . . 14 Fun bday
98 funimaexg 6644 . . . . . . . . . . . . . 14 ((Fun bday 𝐴 ∈ V) → ( bday 𝐴) ∈ V)
9997, 98mpan 688 . . . . . . . . . . . . 13 (𝐴 ∈ V → ( bday 𝐴) ∈ V)
10099uniexd 7753 . . . . . . . . . . . 12 (𝐴 ∈ V → ( bday 𝐴) ∈ V)
101100adantl 480 . . . . . . . . . . 11 ((𝐴 No 𝐴 ∈ V) → ( bday 𝐴) ∈ V)
102 simpl 481 . . . . . . . . . . . . . 14 ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ dom 𝑢)
103102reximi 3081 . . . . . . . . . . . . 13 (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → ∃𝑢𝐴 𝑦 ∈ dom 𝑢)
104103ss2abi 4063 . . . . . . . . . . . 12 {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ {𝑦 ∣ ∃𝑢𝐴 𝑦 ∈ dom 𝑢}
105 bdayval 27601 . . . . . . . . . . . . . . . . . . 19 (𝑢 No → ( bday 𝑢) = dom 𝑢)
10627, 105syl 17 . . . . . . . . . . . . . . . . . 18 ((𝐴 No 𝑢𝐴) → ( bday 𝑢) = dom 𝑢)
107 fofn 6818 . . . . . . . . . . . . . . . . . . . 20 ( bday : No onto→On → bday Fn No )
10895, 107ax-mp 5 . . . . . . . . . . . . . . . . . . 19 bday Fn No
109 fnfvima 7251 . . . . . . . . . . . . . . . . . . 19 (( bday Fn No 𝐴 No 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
110108, 109mp3an1 1444 . . . . . . . . . . . . . . . . . 18 ((𝐴 No 𝑢𝐴) → ( bday 𝑢) ∈ ( bday 𝐴))
111106, 110eqeltrrd 2830 . . . . . . . . . . . . . . . . 17 ((𝐴 No 𝑢𝐴) → dom 𝑢 ∈ ( bday 𝐴))
112 elssuni 4944 . . . . . . . . . . . . . . . . 17 (dom 𝑢 ∈ ( bday 𝐴) → dom 𝑢 ( bday 𝐴))
113111, 112syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 No 𝑢𝐴) → dom 𝑢 ( bday 𝐴))
114113sseld 3981 . . . . . . . . . . . . . . 15 ((𝐴 No 𝑢𝐴) → (𝑦 ∈ dom 𝑢𝑦 ( bday 𝐴)))
115114rexlimdva 3152 . . . . . . . . . . . . . 14 (𝐴 No → (∃𝑢𝐴 𝑦 ∈ dom 𝑢𝑦 ( bday 𝐴)))
116115abssdv 4065 . . . . . . . . . . . . 13 (𝐴 No → {𝑦 ∣ ∃𝑢𝐴 𝑦 ∈ dom 𝑢} ⊆ ( bday 𝐴))
117116adantr 479 . . . . . . . . . . . 12 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 𝑦 ∈ dom 𝑢} ⊆ ( bday 𝐴))
118104, 117sstrid 3993 . . . . . . . . . . 11 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ ( bday 𝐴))
119101, 118ssexd 5328 . . . . . . . . . 10 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ V)
120 elong 6382 . . . . . . . . . 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 256 . . . . . . . 8 ((𝐴 No 𝐴 ∈ V) → {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ∈ On)
12326, 122eqeltrid 2833 . . . . . . 7 ((𝐴 No 𝐴 ∈ V) → dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ∈ On)
124123adantl 480 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ∈ On)
12525rnmpt 5961 . . . . . . . 8 ran (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑧 ∣ ∃𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))}
126 vex 3477 . . . . . . . . . . . 12 𝑔 ∈ V
127 eleq1w 2812 . . . . . . . . . . . . . 14 (𝑦 = 𝑔 → (𝑦 ∈ dom 𝑢𝑔 ∈ dom 𝑢))
128 suceq 6440 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑔 → suc 𝑦 = suc 𝑔)
129128reseq2d 5989 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑔 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝑔))
130128reseq2d 5989 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑔 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑔))
131129, 130eqeq12d 2744 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑔 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))
132131imbi2d 339 . . . . . . . . . . . . . . 15 (𝑦 = 𝑔 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
133132ralbidv 3175 . . . . . . . . . . . . . 14 (𝑦 = 𝑔 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
134127, 133anbi12d 630 . . . . . . . . . . . . 13 (𝑦 = 𝑔 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))))
135134rexbidv 3176 . . . . . . . . . . . 12 (𝑦 = 𝑔 → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))))
136126, 135elab 3669 . . . . . . . . . . 11 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))))
137 eqid 2728 . . . . . . . . . . . . . . . . . . 19 (𝑢𝑔) = (𝑢𝑔)
138 fvex 6915 . . . . . . . . . . . . . . . . . . . 20 (𝑢𝑔) ∈ V
139 eqeq2 2740 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑢𝑔) → ((𝑢𝑔) = 𝑥 ↔ (𝑢𝑔) = (𝑢𝑔)))
1401393anbi3d 1438 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = (𝑢𝑔) → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = (𝑢𝑔))))
141138, 140spcev 3595 . . . . . . . . . . . . . . . . . . 19 ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = (𝑢𝑔)) → ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
142137, 141mp3an3 1446 . . . . . . . . . . . . . . . . . 18 ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
143142reximi 3081 . . . . . . . . . . . . . . . . 17 (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑢𝐴𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
144 rexcom4 3283 . . . . . . . . . . . . . . . . 17 (∃𝑢𝐴𝑥(𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ ∃𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
145143, 144sylib 217 . . . . . . . . . . . . . . . 16 (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔))) → ∃𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
146145adantl 480 . . . . . . . . . . . . . . 15 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
147 nosupprefixmo 27653 . . . . . . . . . . . . . . . 16 (𝐴 No → ∃*𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
148147adantr 479 . . . . . . . . . . . . . . 15 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃*𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
149 df-eu 2558 . . . . . . . . . . . . . . 15 (∃!𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ (∃𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ∧ ∃*𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
150146, 148, 149sylanbrc 581 . . . . . . . . . . . . . 14 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → ∃!𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))
151 vex 3477 . . . . . . . . . . . . . . 15 𝑧 ∈ V
152 eqeq2 2740 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → ((𝑢𝑔) = 𝑥 ↔ (𝑢𝑔) = 𝑧))
1531523anbi3d 1438 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑧 → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧)))
154153rexbidv 3176 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑧 → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧)))
155154iota2 6542 . . . . . . . . . . . . . . 15 ((𝑧 ∈ V ∧ ∃!𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) ↔ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) = 𝑧))
156151, 155mpan 688 . . . . . . . . . . . . . 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 2735 . . . . . . . . . . . . 13 ((℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) = 𝑧𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
159157, 158bitrdi 286 . . . . . . . . . . . 12 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) ↔ 𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
160 simprr3 1220 . . . . . . . . . . . . . . 15 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → (𝑢𝑔) = 𝑧)
16127adantrr 715 . . . . . . . . . . . . . . . . 17 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → 𝑢 No )
162 norn 27604 . . . . . . . . . . . . . . . . 17 (𝑢 No → ran 𝑢 ⊆ {1o, 2o})
163161, 162syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → ran 𝑢 ⊆ {1o, 2o})
164 nofun 27602 . . . . . . . . . . . . . . . . . 18 (𝑢 No → Fun 𝑢)
165161, 164syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → Fun 𝑢)
166 simprr1 1218 . . . . . . . . . . . . . . . . 17 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → 𝑔 ∈ dom 𝑢)
167 fvelrn 7091 . . . . . . . . . . . . . . . . 17 ((Fun 𝑢𝑔 ∈ dom 𝑢) → (𝑢𝑔) ∈ ran 𝑢)
168165, 166, 167syl2anc 582 . . . . . . . . . . . . . . . 16 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → (𝑢𝑔) ∈ ran 𝑢)
169163, 168sseldd 3983 . . . . . . . . . . . . . . 15 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → (𝑢𝑔) ∈ {1o, 2o})
170160, 169eqeltrrd 2830 . . . . . . . . . . . . . 14 ((𝐴 No ∧ (𝑢𝐴 ∧ (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧))) → 𝑧 ∈ {1o, 2o})
171170rexlimdvaa 3153 . . . . . . . . . . . . 13 (𝐴 No → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) → 𝑧 ∈ {1o, 2o}))
172171adantr 479 . . . . . . . . . . . 12 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑧) → 𝑧 ∈ {1o, 2o}))
173159, 172sylbird 259 . . . . . . . . . . 11 ((𝐴 No ∧ ∃𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)))) → (𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) → 𝑧 ∈ {1o, 2o}))
174136, 173sylan2b 592 . . . . . . . . . 10 ((𝐴 No 𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) → (𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) → 𝑧 ∈ {1o, 2o}))
175174rexlimdva 3152 . . . . . . . . 9 (𝐴 No → (∃𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) → 𝑧 ∈ {1o, 2o}))
176175abssdv 4065 . . . . . . . 8 (𝐴 No → {𝑧 ∣ ∃𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}𝑧 = (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))} ⊆ {1o, 2o})
177125, 176eqsstrid 4030 . . . . . . 7 (𝐴 No → ran (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ⊆ {1o, 2o})
178177ad2antrl 726 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → ran (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ⊆ {1o, 2o})
179 elno2 27607 . . . . . 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 1340 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) ∈ No )
18121, 180eqeltrd 2829 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V)) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) ∈ No )
18219, 181pm2.61ian 810 . . 3 ((𝐴 No 𝐴 ∈ V) → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) ∈ No )
1832, 182eqeltrid 2833 . 2 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
1841, 183sylan2 591 1 ((𝐴 No 𝐴𝑉) → 𝑆 No )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084  wal 1531   = wceq 1533  wex 1773  wcel 2098  ∃*wmo 2527  ∃!weu 2557  {cab 2705  wral 3058  wrex 3067  ∃!wreu 3372  ∃*wrmo 3373  Vcvv 3473  cun 3947  wss 3949  ifcif 4532  {csn 4632  {cpr 4634  cop 4638   cuni 4912   class class class wbr 5152  cmpt 5235  Tr wtr 5269  dom cdm 5682  ran crn 5683  cres 5684  cima 5685  Ord word 6373  Oncon0 6374  suc csuc 6376  cio 6503  Fun wfun 6547   Fn wfn 6548  ontowfo 6551  cfv 6553  crio 7381  1oc1o 8486  2oc2o 8487   No csur 27593   <s cslt 27594   bday cbday 27595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-ord 6377  df-on 6378  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-1o 8493  df-2o 8494  df-no 27596  df-slt 27597  df-bday 27598
This theorem is referenced by:  nosupbday  27658  nosupres  27660  nosupbnd1lem1  27661  nosupbnd1lem2  27662  nosupbnd1lem3  27663  nosupbnd1lem4  27664  nosupbnd1lem5  27665  nosupbnd1lem6  27666  nosupbnd2  27669  nosupinfsep  27685  noetasuplem1  27686  noetasuplem2  27687  noetasuplem3  27688  noetasuplem4  27689  noetalem1  27694
  Copyright terms: Public domain W3C validator