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

Theorem noinfres 33491
 Description: The restriction of surreal infimum when there is no minimum. (Contributed by Scott Fenton, 8-Aug-2024.)
Hypothesis
Ref Expression
noinfres.1 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
Assertion
Ref Expression
noinfres ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑇 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))
Distinct variable groups:   𝐵,𝑔,𝑢,𝑣,𝑥,𝑦   𝑣,𝐺   𝑥,𝑔,𝑦   𝑢,𝑈,𝑣,𝑥   𝑦,𝑢   𝑔,𝑉   𝑥,𝑣,𝑦
Allowed substitution hints:   𝑇(𝑥,𝑦,𝑣,𝑢,𝑔)   𝑈(𝑦,𝑔)   𝐺(𝑥,𝑦,𝑢,𝑔)   𝑉(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem noinfres
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmres 5846 . . . 4 dom (𝑇 ↾ suc 𝐺) = (suc 𝐺 ∩ dom 𝑇)
2 noinfres.1 . . . . . . . . 9 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
32noinfno 33487 . . . . . . . 8 ((𝐵 No 𝐵𝑉) → 𝑇 No )
433ad2ant2 1132 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝑇 No )
5 nodmord 33422 . . . . . . 7 (𝑇 No → Ord dom 𝑇)
64, 5syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Ord dom 𝑇)
7 simp31 1207 . . . . . . . . 9 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝑈𝐵)
8 simp32 1208 . . . . . . . . 9 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ dom 𝑈)
9 simp33 1209 . . . . . . . . 9 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
10 dmeq 5744 . . . . . . . . . . . 12 (𝑏 = 𝑈 → dom 𝑏 = dom 𝑈)
1110eleq2d 2838 . . . . . . . . . . 11 (𝑏 = 𝑈 → (𝐺 ∈ dom 𝑏𝐺 ∈ dom 𝑈))
12 breq1 5036 . . . . . . . . . . . . . . 15 (𝑏 = 𝑈 → (𝑏 <s 𝑐𝑈 <s 𝑐))
1312notbid 322 . . . . . . . . . . . . . 14 (𝑏 = 𝑈 → (¬ 𝑏 <s 𝑐 ↔ ¬ 𝑈 <s 𝑐))
14 reseq1 5818 . . . . . . . . . . . . . . 15 (𝑏 = 𝑈 → (𝑏 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))
1514eqeq1d 2761 . . . . . . . . . . . . . 14 (𝑏 = 𝑈 → ((𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺) ↔ (𝑈 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)))
1613, 15imbi12d 349 . . . . . . . . . . . . 13 (𝑏 = 𝑈 → ((¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)) ↔ (¬ 𝑈 <s 𝑐 → (𝑈 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))))
1716ralbidv 3127 . . . . . . . . . . . 12 (𝑏 = 𝑈 → (∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)) ↔ ∀𝑐𝐵𝑈 <s 𝑐 → (𝑈 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))))
18 breq2 5037 . . . . . . . . . . . . . . 15 (𝑐 = 𝑣 → (𝑈 <s 𝑐𝑈 <s 𝑣))
1918notbid 322 . . . . . . . . . . . . . 14 (𝑐 = 𝑣 → (¬ 𝑈 <s 𝑐 ↔ ¬ 𝑈 <s 𝑣))
20 reseq1 5818 . . . . . . . . . . . . . . 15 (𝑐 = 𝑣 → (𝑐 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))
2120eqeq2d 2770 . . . . . . . . . . . . . 14 (𝑐 = 𝑣 → ((𝑈 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺) ↔ (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
2219, 21imbi12d 349 . . . . . . . . . . . . 13 (𝑐 = 𝑣 → ((¬ 𝑈 <s 𝑐 → (𝑈 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)) ↔ (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
2322cbvralvw 3362 . . . . . . . . . . . 12 (∀𝑐𝐵𝑈 <s 𝑐 → (𝑈 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)) ↔ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
2417, 23bitrdi 290 . . . . . . . . . . 11 (𝑏 = 𝑈 → (∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)) ↔ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
2511, 24anbi12d 634 . . . . . . . . . 10 (𝑏 = 𝑈 → ((𝐺 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))) ↔ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
2625rspcev 3542 . . . . . . . . 9 ((𝑈𝐵 ∧ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑏𝐵 (𝐺 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))))
277, 8, 9, 26syl12anc 836 . . . . . . . 8 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑏𝐵 (𝐺 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))))
28 eleq1 2840 . . . . . . . . . . . 12 (𝑎 = 𝐺 → (𝑎 ∈ dom 𝑏𝐺 ∈ dom 𝑏))
29 suceq 6235 . . . . . . . . . . . . . . . 16 (𝑎 = 𝐺 → suc 𝑎 = suc 𝐺)
3029reseq2d 5824 . . . . . . . . . . . . . . 15 (𝑎 = 𝐺 → (𝑏 ↾ suc 𝑎) = (𝑏 ↾ suc 𝐺))
3129reseq2d 5824 . . . . . . . . . . . . . . 15 (𝑎 = 𝐺 → (𝑐 ↾ suc 𝑎) = (𝑐 ↾ suc 𝐺))
3230, 31eqeq12d 2775 . . . . . . . . . . . . . 14 (𝑎 = 𝐺 → ((𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎) ↔ (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)))
3332imbi2d 345 . . . . . . . . . . . . 13 (𝑎 = 𝐺 → ((¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)) ↔ (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))))
3433ralbidv 3127 . . . . . . . . . . . 12 (𝑎 = 𝐺 → (∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)) ↔ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))))
3528, 34anbi12d 634 . . . . . . . . . . 11 (𝑎 = 𝐺 → ((𝑎 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎))) ↔ (𝐺 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)))))
3635rexbidv 3222 . . . . . . . . . 10 (𝑎 = 𝐺 → (∃𝑏𝐵 (𝑎 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎))) ↔ ∃𝑏𝐵 (𝐺 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)))))
3736elabg 3588 . . . . . . . . 9 (𝐺 ∈ dom 𝑈 → (𝐺 ∈ {𝑎 ∣ ∃𝑏𝐵 (𝑎 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)))} ↔ ∃𝑏𝐵 (𝐺 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)))))
388, 37syl 17 . . . . . . . 8 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝐺 ∈ {𝑎 ∣ ∃𝑏𝐵 (𝑎 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)))} ↔ ∃𝑏𝐵 (𝐺 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)))))
3927, 38mpbird 260 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ {𝑎 ∣ ∃𝑏𝐵 (𝑎 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)))})
402noinfdm 33488 . . . . . . . 8 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑎 ∣ ∃𝑏𝐵 (𝑎 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)))})
41403ad2ant1 1131 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom 𝑇 = {𝑎 ∣ ∃𝑏𝐵 (𝑎 ∈ dom 𝑏 ∧ ∀𝑐𝐵𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)))})
4239, 41eleqtrrd 2856 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ dom 𝑇)
43 ordsucss 7533 . . . . . 6 (Ord dom 𝑇 → (𝐺 ∈ dom 𝑇 → suc 𝐺 ⊆ dom 𝑇))
446, 42, 43sylc 65 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → suc 𝐺 ⊆ dom 𝑇)
45 df-ss 3876 . . . . 5 (suc 𝐺 ⊆ dom 𝑇 ↔ (suc 𝐺 ∩ dom 𝑇) = suc 𝐺)
4644, 45sylib 221 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (suc 𝐺 ∩ dom 𝑇) = suc 𝐺)
471, 46syl5eq 2806 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom (𝑇 ↾ suc 𝐺) = suc 𝐺)
48 dmres 5846 . . . 4 dom (𝑈 ↾ suc 𝐺) = (suc 𝐺 ∩ dom 𝑈)
49 simp2l 1197 . . . . . . . . 9 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐵 No )
5049, 7sseldd 3894 . . . . . . . 8 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝑈 No )
51 nodmon 33419 . . . . . . . 8 (𝑈 No → dom 𝑈 ∈ On)
5250, 51syl 17 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom 𝑈 ∈ On)
53 eloni 6180 . . . . . . 7 (dom 𝑈 ∈ On → Ord dom 𝑈)
5452, 53syl 17 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Ord dom 𝑈)
55 ordsucss 7533 . . . . . 6 (Ord dom 𝑈 → (𝐺 ∈ dom 𝑈 → suc 𝐺 ⊆ dom 𝑈))
5654, 8, 55sylc 65 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → suc 𝐺 ⊆ dom 𝑈)
57 df-ss 3876 . . . . 5 (suc 𝐺 ⊆ dom 𝑈 ↔ (suc 𝐺 ∩ dom 𝑈) = suc 𝐺)
5856, 57sylib 221 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (suc 𝐺 ∩ dom 𝑈) = suc 𝐺)
5948, 58syl5eq 2806 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom (𝑈 ↾ suc 𝐺) = suc 𝐺)
6047, 59eqtr4d 2797 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom (𝑇 ↾ suc 𝐺) = dom (𝑈 ↾ suc 𝐺))
6147eleq2d 2838 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ dom (𝑇 ↾ suc 𝐺) ↔ 𝑎 ∈ suc 𝐺))
62 simpl1 1189 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥)
63 simpl2 1190 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → (𝐵 No 𝐵𝑉))
64 simpl31 1252 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑈𝐵)
6556sselda 3893 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑎 ∈ dom 𝑈)
6650adantr 485 . . . . . . . . . . . . 13 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑈 No )
6766, 51syl 17 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → dom 𝑈 ∈ On)
68 simpl32 1253 . . . . . . . . . . . 12 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝐺 ∈ dom 𝑈)
69 onelon 6195 . . . . . . . . . . . 12 ((dom 𝑈 ∈ On ∧ 𝐺 ∈ dom 𝑈) → 𝐺 ∈ On)
7067, 68, 69syl2anc 588 . . . . . . . . . . 11 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝐺 ∈ On)
71 sucelon 7532 . . . . . . . . . . 11 (𝐺 ∈ On ↔ suc 𝐺 ∈ On)
7270, 71sylib 221 . . . . . . . . . 10 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → suc 𝐺 ∈ On)
73 eloni 6180 . . . . . . . . . 10 (suc 𝐺 ∈ On → Ord suc 𝐺)
7472, 73syl 17 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → Ord suc 𝐺)
75 simpr 489 . . . . . . . . 9 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑎 ∈ suc 𝐺)
76 ordsucss 7533 . . . . . . . . 9 (Ord suc 𝐺 → (𝑎 ∈ suc 𝐺 → suc 𝑎 ⊆ suc 𝐺))
7774, 75, 76sylc 65 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → suc 𝑎 ⊆ suc 𝐺)
78 simpl33 1254 . . . . . . . 8 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
79 reseq1 5818 . . . . . . . . . . 11 ((𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) → ((𝑈 ↾ suc 𝐺) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝐺) ↾ suc 𝑎))
80 resabs1 5854 . . . . . . . . . . . 12 (suc 𝑎 ⊆ suc 𝐺 → ((𝑈 ↾ suc 𝐺) ↾ suc 𝑎) = (𝑈 ↾ suc 𝑎))
81 resabs1 5854 . . . . . . . . . . . 12 (suc 𝑎 ⊆ suc 𝐺 → ((𝑣 ↾ suc 𝐺) ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))
8280, 81eqeq12d 2775 . . . . . . . . . . 11 (suc 𝑎 ⊆ suc 𝐺 → (((𝑈 ↾ suc 𝐺) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝐺) ↾ suc 𝑎) ↔ (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
8379, 82syl5ib 247 . . . . . . . . . 10 (suc 𝑎 ⊆ suc 𝐺 → ((𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
8483imim2d 57 . . . . . . . . 9 (suc 𝑎 ⊆ suc 𝐺 → ((¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) → (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
8584ralimdv 3110 . . . . . . . 8 (suc 𝑎 ⊆ suc 𝐺 → (∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) → ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))))
8677, 78, 85sylc 65 . . . . . . 7 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))
872noinffv 33490 . . . . . . 7 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝑎 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))) → (𝑇𝑎) = (𝑈𝑎))
8862, 63, 64, 65, 86, 87syl113anc 1380 . . . . . 6 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → (𝑇𝑎) = (𝑈𝑎))
8975fvresd 6679 . . . . . 6 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ((𝑇 ↾ suc 𝐺)‘𝑎) = (𝑇𝑎))
9075fvresd 6679 . . . . . 6 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ((𝑈 ↾ suc 𝐺)‘𝑎) = (𝑈𝑎))
9188, 89, 903eqtr4d 2804 . . . . 5 (((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ((𝑇 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))
9291ex 417 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ suc 𝐺 → ((𝑇 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎)))
9361, 92sylbid 243 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ dom (𝑇 ↾ suc 𝐺) → ((𝑇 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎)))
9493ralrimiv 3113 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∀𝑎 ∈ dom (𝑇 ↾ suc 𝐺)((𝑇 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))
95 nofun 33418 . . . . 5 (𝑇 No → Fun 𝑇)
9695funresd 6379 . . . 4 (𝑇 No → Fun (𝑇 ↾ suc 𝐺))
974, 96syl 17 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Fun (𝑇 ↾ suc 𝐺))
98 nofun 33418 . . . . 5 (𝑈 No → Fun 𝑈)
9998funresd 6379 . . . 4 (𝑈 No → Fun (𝑈 ↾ suc 𝐺))
10050, 99syl 17 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Fun (𝑈 ↾ suc 𝐺))
101 eqfunfv 6799 . . 3 ((Fun (𝑇 ↾ suc 𝐺) ∧ Fun (𝑈 ↾ suc 𝐺)) → ((𝑇 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺) ↔ (dom (𝑇 ↾ suc 𝐺) = dom (𝑈 ↾ suc 𝐺) ∧ ∀𝑎 ∈ dom (𝑇 ↾ suc 𝐺)((𝑇 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))))
10297, 100, 101syl2anc 588 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ((𝑇 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺) ↔ (dom (𝑇 ↾ suc 𝐺) = dom (𝑈 ↾ suc 𝐺) ∧ ∀𝑎 ∈ dom (𝑇 ↾ suc 𝐺)((𝑇 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))))
10360, 94, 102mpbir2and 713 1 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑇 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  {cab 2736  ∀wral 3071  ∃wrex 3072   ∪ cun 3857   ∩ cin 3858   ⊆ wss 3859  ifcif 4421  {csn 4523  ⟨cop 4529   class class class wbr 5033   ↦ cmpt 5113  dom cdm 5525   ↾ cres 5527  Ord word 6169  Oncon0 6170  suc csuc 6172  ℩cio 6293  Fun wfun 6330  ‘cfv 6336  ℩crio 7108  1oc1o 8106   No csur 33409
 Copyright terms: Public domain W3C validator