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

Theorem nosupres 32080
Description: A restriction law for surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021.)
Hypothesis
Ref Expression
nosupres.1 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
nosupres ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑆 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))
Distinct variable groups:   𝐴,𝑔,𝑢,𝑣,𝑥,𝑦   𝑢,𝐺   𝑣,𝑔   𝑣,𝐺   𝑥,𝑔,𝑦   𝑦,𝐺   𝑢,𝑈,𝑣,𝑥   𝑦,𝑢   𝑥,𝑣,𝑦
Allowed substitution hints:   𝑆(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑈(𝑦,𝑔)   𝐺(𝑥,𝑔)

Proof of Theorem nosupres
Dummy variables 𝑎 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmres 5529 . . . 4 dom (𝑆 ↾ suc 𝐺) = (suc 𝐺 ∩ dom 𝑆)
2 nosupres.1 . . . . . . . . 9 𝑆 = if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
32nosupno 32076 . . . . . . . 8 ((𝐴 No 𝐴 ∈ V) → 𝑆 No )
433ad2ant2 1126 . . . . . . 7 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝑆 No )
5 nodmord 32033 . . . . . . 7 (𝑆 No → Ord dom 𝑆)
64, 5syl 17 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Ord dom 𝑆)
7 dmeq 5431 . . . . . . . . . . . . . 14 (𝑝 = 𝑈 → dom 𝑝 = dom 𝑈)
87eleq2d 2789 . . . . . . . . . . . . 13 (𝑝 = 𝑈 → (𝐺 ∈ dom 𝑝𝐺 ∈ dom 𝑈))
9 breq2 4764 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑈 → (𝑣 <s 𝑝𝑣 <s 𝑈))
109notbid 307 . . . . . . . . . . . . . . 15 (𝑝 = 𝑈 → (¬ 𝑣 <s 𝑝 ↔ ¬ 𝑣 <s 𝑈))
11 reseq1 5497 . . . . . . . . . . . . . . . 16 (𝑝 = 𝑈 → (𝑝 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))
1211eqeq1d 2726 . . . . . . . . . . . . . . 15 (𝑝 = 𝑈 → ((𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
1310, 12imbi12d 333 . . . . . . . . . . . . . 14 (𝑝 = 𝑈 → ((¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
1413ralbidv 3088 . . . . . . . . . . . . 13 (𝑝 = 𝑈 → (∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
158, 14anbi12d 749 . . . . . . . . . . . 12 (𝑝 = 𝑈 → ((𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) ↔ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
1615rspcev 3413 . . . . . . . . . . 11 ((𝑈𝐴 ∧ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
17163impb 1107 . . . . . . . . . 10 ((𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
18 dmeq 5431 . . . . . . . . . . . . 13 (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
1918eleq2d 2789 . . . . . . . . . . . 12 (𝑢 = 𝑝 → (𝐺 ∈ dom 𝑢𝐺 ∈ dom 𝑝))
20 breq2 4764 . . . . . . . . . . . . . . 15 (𝑢 = 𝑝 → (𝑣 <s 𝑢𝑣 <s 𝑝))
2120notbid 307 . . . . . . . . . . . . . 14 (𝑢 = 𝑝 → (¬ 𝑣 <s 𝑢 ↔ ¬ 𝑣 <s 𝑝))
22 reseq1 5497 . . . . . . . . . . . . . . 15 (𝑢 = 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
2322eqeq1d 2726 . . . . . . . . . . . . . 14 (𝑢 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
2421, 23imbi12d 333 . . . . . . . . . . . . 13 (𝑢 = 𝑝 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
2524ralbidv 3088 . . . . . . . . . . . 12 (𝑢 = 𝑝 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
2619, 25anbi12d 749 . . . . . . . . . . 11 (𝑢 = 𝑝 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) ↔ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
2726cbvrexv 3275 . . . . . . . . . 10 (∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) ↔ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
2817, 27sylibr 224 . . . . . . . . 9 ((𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
29 eleq1 2791 . . . . . . . . . . . . 13 (𝑦 = 𝐺 → (𝑦 ∈ dom 𝑢𝐺 ∈ dom 𝑢))
30 suceq 5903 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝐺 → suc 𝑦 = suc 𝐺)
3130reseq2d 5503 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐺 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝐺))
3230reseq2d 5503 . . . . . . . . . . . . . . . 16 (𝑦 = 𝐺 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝐺))
3331, 32eqeq12d 2739 . . . . . . . . . . . . . . 15 (𝑦 = 𝐺 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
3433imbi2d 329 . . . . . . . . . . . . . 14 (𝑦 = 𝐺 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
3534ralbidv 3088 . . . . . . . . . . . . 13 (𝑦 = 𝐺 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
3629, 35anbi12d 749 . . . . . . . . . . . 12 (𝑦 = 𝐺 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
3736rexbidv 3154 . . . . . . . . . . 11 (𝑦 = 𝐺 → (∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
3837elabg 3456 . . . . . . . . . 10 (𝐺 ∈ dom 𝑈 → (𝐺 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
39383ad2ant2 1126 . . . . . . . . 9 ((𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → (𝐺 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
4028, 39mpbird 247 . . . . . . . 8 ((𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → 𝐺 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
41403ad2ant3 1127 . . . . . . 7 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
42 iffalse 4203 . . . . . . . . . . 11 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦, ((𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦) ∪ {⟨dom (𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦), 2𝑜⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
432, 42syl5eq 2770 . . . . . . . . . 10 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
4443dmeqd 5433 . . . . . . . . 9 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
45 iotaex 5981 . . . . . . . . . 10 (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) ∈ V
46 eqid 2724 . . . . . . . . . 10 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
4745, 46dmmpti 6136 . . . . . . . . 9 dom (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}
4844, 47syl6eq 2774 . . . . . . . 8 (¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
49483ad2ant1 1125 . . . . . . 7 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom 𝑆 = {𝑦 ∣ ∃𝑢𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
5041, 49eleqtrrd 2806 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ dom 𝑆)
51 ordsucss 7135 . . . . . 6 (Ord dom 𝑆 → (𝐺 ∈ dom 𝑆 → suc 𝐺 ⊆ dom 𝑆))
526, 50, 51sylc 65 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → suc 𝐺 ⊆ dom 𝑆)
53 df-ss 3694 . . . . 5 (suc 𝐺 ⊆ dom 𝑆 ↔ (suc 𝐺 ∩ dom 𝑆) = suc 𝐺)
5452, 53sylib 208 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (suc 𝐺 ∩ dom 𝑆) = suc 𝐺)
551, 54syl5eq 2770 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom (𝑆 ↾ suc 𝐺) = suc 𝐺)
56 dmres 5529 . . . 4 dom (𝑈 ↾ suc 𝐺) = (suc 𝐺 ∩ dom 𝑈)
57 simp2l 1218 . . . . . . . 8 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐴 No )
58 simp31 1228 . . . . . . . 8 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝑈𝐴)
5957, 58sseldd 3710 . . . . . . 7 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝑈 No )
60 nodmord 32033 . . . . . . 7 (𝑈 No → Ord dom 𝑈)
6159, 60syl 17 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Ord dom 𝑈)
62 simp32 1229 . . . . . 6 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ dom 𝑈)
63 ordsucss 7135 . . . . . 6 (Ord dom 𝑈 → (𝐺 ∈ dom 𝑈 → suc 𝐺 ⊆ dom 𝑈))
6461, 62, 63sylc 65 . . . . 5 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → suc 𝐺 ⊆ dom 𝑈)
65 df-ss 3694 . . . . 5 (suc 𝐺 ⊆ dom 𝑈 ↔ (suc 𝐺 ∩ dom 𝑈) = suc 𝐺)
6664, 65sylib 208 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (suc 𝐺 ∩ dom 𝑈) = suc 𝐺)
6756, 66syl5eq 2770 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom (𝑈 ↾ suc 𝐺) = suc 𝐺)
6855, 67eqtr4d 2761 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom (𝑆 ↾ suc 𝐺) = dom (𝑈 ↾ suc 𝐺))
6955eleq2d 2789 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ dom (𝑆 ↾ suc 𝐺) ↔ 𝑎 ∈ suc 𝐺))
70 simpl1 1204 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦)
71 simpl2 1206 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → (𝐴 No 𝐴 ∈ V))
72 simpl31 1291 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑈𝐴)
7364sselda 3709 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑎 ∈ dom 𝑈)
74 nodmon 32030 . . . . . . . . . . . . . 14 (𝑈 No → dom 𝑈 ∈ On)
7559, 74syl 17 . . . . . . . . . . . . 13 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom 𝑈 ∈ On)
76 onelon 5861 . . . . . . . . . . . . 13 ((dom 𝑈 ∈ On ∧ 𝐺 ∈ dom 𝑈) → 𝐺 ∈ On)
7775, 62, 76syl2anc 696 . . . . . . . . . . . 12 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ On)
78 eloni 5846 . . . . . . . . . . . 12 (𝐺 ∈ On → Ord 𝐺)
7977, 78syl 17 . . . . . . . . . . 11 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Ord 𝐺)
80 ordsuc 7131 . . . . . . . . . . 11 (Ord 𝐺 ↔ Ord suc 𝐺)
8179, 80sylib 208 . . . . . . . . . 10 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Ord suc 𝐺)
82 ordsucss 7135 . . . . . . . . . 10 (Ord suc 𝐺 → (𝑎 ∈ suc 𝐺 → suc 𝑎 ⊆ suc 𝐺))
8381, 82syl 17 . . . . . . . . 9 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ suc 𝐺 → suc 𝑎 ⊆ suc 𝐺))
8483imp 444 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → suc 𝑎 ⊆ suc 𝐺)
85 simpl33 1293 . . . . . . . 8 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
86 reseq1 5497 . . . . . . . . . . 11 ((𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) → ((𝑈 ↾ suc 𝐺) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝐺) ↾ suc 𝑎))
87 resabs1 5537 . . . . . . . . . . . 12 (suc 𝑎 ⊆ suc 𝐺 → ((𝑈 ↾ suc 𝐺) ↾ suc 𝑎) = (𝑈 ↾ suc 𝑎))
88 resabs1 5537 . . . . . . . . . . . 12 (suc 𝑎 ⊆ suc 𝐺 → ((𝑣 ↾ suc 𝐺) ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))
8987, 88eqeq12d 2739 . . . . . . . . . . 11 (suc 𝑎 ⊆ suc 𝐺 → (((𝑈 ↾ suc 𝐺) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝐺) ↾ suc 𝑎) ↔ (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
9086, 89syl5ib 234 . . . . . . . . . 10 (suc 𝑎 ⊆ suc 𝐺 → ((𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
9190imim2d 57 . . . . . . . . 9 (suc 𝑎 ⊆ suc 𝐺 → ((¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) → (¬ 𝑣 <s 𝑈 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
9291ralimdv 3065 . . . . . . . 8 (suc 𝑎 ⊆ suc 𝐺 → (∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) → ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
9384, 85, 92sylc 65 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
942nosupfv 32079 . . . . . . 7 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝑎 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))) → (𝑆𝑎) = (𝑈𝑎))
9570, 71, 72, 73, 93, 94syl113anc 1451 . . . . . 6 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → (𝑆𝑎) = (𝑈𝑎))
96 simpr 479 . . . . . . 7 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑎 ∈ suc 𝐺)
9796fvresd 6321 . . . . . 6 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ((𝑆 ↾ suc 𝐺)‘𝑎) = (𝑆𝑎))
9896fvresd 6321 . . . . . 6 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ((𝑈 ↾ suc 𝐺)‘𝑎) = (𝑈𝑎))
9995, 97, 983eqtr4d 2768 . . . . 5 (((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ((𝑆 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))
10099ex 449 . . . 4 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ suc 𝐺 → ((𝑆 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎)))
10169, 100sylbid 230 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ dom (𝑆 ↾ suc 𝐺) → ((𝑆 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎)))
102101ralrimiv 3067 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∀𝑎 ∈ dom (𝑆 ↾ suc 𝐺)((𝑆 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))
103 nofun 32029 . . . 4 (𝑆 No → Fun 𝑆)
104 funres 6042 . . . 4 (Fun 𝑆 → Fun (𝑆 ↾ suc 𝐺))
1054, 103, 1043syl 18 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Fun (𝑆 ↾ suc 𝐺))
106 nofun 32029 . . . 4 (𝑈 No → Fun 𝑈)
107 funres 6042 . . . 4 (Fun 𝑈 → Fun (𝑈 ↾ suc 𝐺))
10859, 106, 1073syl 18 . . 3 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Fun (𝑈 ↾ suc 𝐺))
109 eqfunfv 6431 . . 3 ((Fun (𝑆 ↾ suc 𝐺) ∧ Fun (𝑈 ↾ suc 𝐺)) → ((𝑆 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺) ↔ (dom (𝑆 ↾ suc 𝐺) = dom (𝑈 ↾ suc 𝐺) ∧ ∀𝑎 ∈ dom (𝑆 ↾ suc 𝐺)((𝑆 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))))
110105, 108, 109syl2anc 696 . 2 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ((𝑆 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺) ↔ (dom (𝑆 ↾ suc 𝐺) = dom (𝑈 ↾ suc 𝐺) ∧ ∀𝑎 ∈ dom (𝑆 ↾ suc 𝐺)((𝑆 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))))
11168, 102, 110mpbir2and 995 1 ((¬ ∃𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 No 𝐴 ∈ V) ∧ (𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐴𝑣 <s 𝑈 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑆 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1596  wcel 2103  {cab 2710  wral 3014  wrex 3015  Vcvv 3304  cun 3678  cin 3679  wss 3680  ifcif 4194  {csn 4285  cop 4291   class class class wbr 4760  cmpt 4837  dom cdm 5218  cres 5220  Ord word 5835  Oncon0 5836  suc csuc 5838  cio 5962  Fun wfun 5995  cfv 6001  crio 6725  2𝑜c2o 7674   No csur 32020   <s cslt 32021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-ord 5839  df-on 5840  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-1o 7680  df-2o 7681  df-no 32023  df-slt 32024  df-bday 32025
This theorem is referenced by:  nosupbnd1lem1  32081  nosupbnd2  32089
  Copyright terms: Public domain W3C validator