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

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

Proof of Theorem noinffv
StepHypRef Expression
1 noinffv.1 . . . . 5 𝑇 = if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
2 iffalse 4432 . . . . 5 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → if(∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥, ((𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥) ∪ {⟨dom (𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥), 1o⟩}), (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
31, 2syl5eq 2805 . . . 4 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥𝑇 = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))))
43fveq1d 6665 . . 3 (¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 → (𝑇𝐺) = ((𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))‘𝐺))
543ad2ant1 1130 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑇𝐺) = ((𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))‘𝐺))
6 dmeq 5749 . . . . . . . . 9 (𝑢 = 𝑈 → dom 𝑢 = dom 𝑈)
76eleq2d 2837 . . . . . . . 8 (𝑢 = 𝑈 → (𝐺 ∈ dom 𝑢𝐺 ∈ dom 𝑈))
8 breq1 5039 . . . . . . . . . . 11 (𝑢 = 𝑈 → (𝑢 <s 𝑣𝑈 <s 𝑣))
98notbid 321 . . . . . . . . . 10 (𝑢 = 𝑈 → (¬ 𝑢 <s 𝑣 ↔ ¬ 𝑈 <s 𝑣))
10 reseq1 5822 . . . . . . . . . . 11 (𝑢 = 𝑈 → (𝑢 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺))
1110eqeq1d 2760 . . . . . . . . . 10 (𝑢 = 𝑈 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
129, 11imbi12d 348 . . . . . . . . 9 (𝑢 = 𝑈 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
1312ralbidv 3126 . . . . . . . 8 (𝑢 = 𝑈 → (∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
147, 13anbi12d 633 . . . . . . 7 (𝑢 = 𝑈 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) ↔ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
1514rspcev 3543 . . . . . 6 ((𝑈𝐵 ∧ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
16153impb 1112 . . . . 5 ((𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
17163ad2ant3 1132 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
18 simp32 1207 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ dom 𝑈)
19 eleq1 2839 . . . . . . . 8 (𝑦 = 𝐺 → (𝑦 ∈ dom 𝑢𝐺 ∈ dom 𝑢))
20 suceq 6239 . . . . . . . . . . . 12 (𝑦 = 𝐺 → suc 𝑦 = suc 𝐺)
2120reseq2d 5828 . . . . . . . . . . 11 (𝑦 = 𝐺 → (𝑢 ↾ suc 𝑦) = (𝑢 ↾ suc 𝐺))
2220reseq2d 5828 . . . . . . . . . . 11 (𝑦 = 𝐺 → (𝑣 ↾ suc 𝑦) = (𝑣 ↾ suc 𝐺))
2321, 22eqeq12d 2774 . . . . . . . . . 10 (𝑦 = 𝐺 → ((𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦) ↔ (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
2423imbi2d 344 . . . . . . . . 9 (𝑦 = 𝐺 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
2524ralbidv 3126 . . . . . . . 8 (𝑦 = 𝐺 → (∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)) ↔ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
2619, 25anbi12d 633 . . . . . . 7 (𝑦 = 𝐺 → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
2726rexbidv 3221 . . . . . 6 (𝑦 = 𝐺 → (∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) ↔ ∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
2827elabg 3589 . . . . 5 (𝐺 ∈ dom 𝑈 → (𝐺 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
2918, 28syl 17 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝐺 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↔ ∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))))
3017, 29mpbird 260 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))})
31 eleq1 2839 . . . . . . 7 (𝑔 = 𝐺 → (𝑔 ∈ dom 𝑢𝐺 ∈ dom 𝑢))
32 suceq 6239 . . . . . . . . . . 11 (𝑔 = 𝐺 → suc 𝑔 = suc 𝐺)
3332reseq2d 5828 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑢 ↾ suc 𝑔) = (𝑢 ↾ suc 𝐺))
3432reseq2d 5828 . . . . . . . . . 10 (𝑔 = 𝐺 → (𝑣 ↾ suc 𝑔) = (𝑣 ↾ suc 𝐺))
3533, 34eqeq12d 2774 . . . . . . . . 9 (𝑔 = 𝐺 → ((𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔) ↔ (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
3635imbi2d 344 . . . . . . . 8 (𝑔 = 𝐺 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
3736ralbidv 3126 . . . . . . 7 (𝑔 = 𝐺 → (∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ↔ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
38 fveqeq2 6672 . . . . . . 7 (𝑔 = 𝐺 → ((𝑢𝑔) = 𝑥 ↔ (𝑢𝐺) = 𝑥))
3931, 37, 383anbi123d 1433 . . . . . 6 (𝑔 = 𝐺 → ((𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥)))
4039rexbidv 3221 . . . . 5 (𝑔 = 𝐺 → (∃𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥) ↔ ∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥)))
4140iotabidv 6324 . . . 4 (𝑔 = 𝐺 → (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)) = (℩𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥)))
42 eqid 2758 . . . 4 (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))
43 iotaex 6320 . . . 4 (℩𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥)) ∈ V
4441, 42, 43fvmpt 6764 . . 3 (𝐺 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} → ((𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))‘𝐺) = (℩𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥)))
4530, 44syl 17 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ((𝑔 ∈ {𝑦 ∣ ∃𝑢𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥𝑢𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢𝑔) = 𝑥)))‘𝐺) = (℩𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥)))
46 simp1 1133 . . . . 5 ((𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → 𝑈𝐵)
47 simp2 1134 . . . . 5 ((𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → 𝐺 ∈ dom 𝑈)
48 simp3 1135 . . . . 5 ((𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
49 eqidd 2759 . . . . 5 ((𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → (𝑈𝐺) = (𝑈𝐺))
50 fveq1 6662 . . . . . . . 8 (𝑢 = 𝑈 → (𝑢𝐺) = (𝑈𝐺))
5150eqeq1d 2760 . . . . . . 7 (𝑢 = 𝑈 → ((𝑢𝐺) = (𝑈𝐺) ↔ (𝑈𝐺) = (𝑈𝐺)))
527, 13, 513anbi123d 1433 . . . . . 6 (𝑢 = 𝑈 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = (𝑈𝐺)) ↔ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑈𝐺) = (𝑈𝐺))))
5352rspcev 3543 . . . . 5 ((𝑈𝐵 ∧ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑈𝐺) = (𝑈𝐺))) → ∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = (𝑈𝐺)))
5446, 47, 48, 49, 53syl13anc 1369 . . . 4 ((𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = (𝑈𝐺)))
55543ad2ant3 1132 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = (𝑈𝐺)))
56 fvex 6676 . . . 4 (𝑈𝐺) ∈ V
57 eqid 2758 . . . . . . . . . 10 (𝑢𝐺) = (𝑢𝐺)
58 fvex 6676 . . . . . . . . . . 11 (𝑢𝐺) ∈ V
59 eqeq2 2770 . . . . . . . . . . . 12 (𝑥 = (𝑢𝐺) → ((𝑢𝐺) = 𝑥 ↔ (𝑢𝐺) = (𝑢𝐺)))
60593anbi3d 1439 . . . . . . . . . . 11 (𝑥 = (𝑢𝐺) → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = (𝑢𝐺))))
6158, 60spcev 3527 . . . . . . . . . 10 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = (𝑢𝐺)) → ∃𝑥(𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
6257, 61mp3an3 1447 . . . . . . . . 9 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑥(𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
6362reximi 3171 . . . . . . . 8 (∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑢𝐵𝑥(𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
64 rexcom4 3177 . . . . . . . 8 (∃𝑢𝐵𝑥(𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ ∃𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
6563, 64sylib 221 . . . . . . 7 (∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
6616, 65syl 17 . . . . . 6 ((𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) → ∃𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
67663ad2ant3 1132 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
68 simp2l 1196 . . . . . 6 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐵 No )
69 noinfprefixmo 33501 . . . . . 6 (𝐵 No → ∃*𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
7068, 69syl 17 . . . . 5 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃*𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
71 df-eu 2588 . . . . 5 (∃!𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ (∃𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ ∃*𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥)))
7267, 70, 71sylanbrc 586 . . . 4 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃!𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
73 eqeq2 2770 . . . . . . 7 (𝑥 = (𝑈𝐺) → ((𝑢𝐺) = 𝑥 ↔ (𝑢𝐺) = (𝑈𝐺)))
74733anbi3d 1439 . . . . . 6 (𝑥 = (𝑈𝐺) → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = (𝑈𝐺))))
7574rexbidv 3221 . . . . 5 (𝑥 = (𝑈𝐺) → (∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ ∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = (𝑈𝐺))))
7675iota2 6329 . . . 4 (((𝑈𝐺) ∈ V ∧ ∃!𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥)) → (∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = (𝑈𝐺)) ↔ (℩𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥)) = (𝑈𝐺)))
7756, 72, 76sylancr 590 . . 3 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (∃𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = (𝑈𝐺)) ↔ (℩𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥)) = (𝑈𝐺)))
7855, 77mpbid 235 . 2 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (℩𝑥𝑢𝐵 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐵𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥)) = (𝑈𝐺))
795, 45, 783eqtrd 2797 1 ((¬ ∃𝑥𝐵𝑦𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 No 𝐵𝑉) ∧ (𝑈𝐵𝐺 ∈ dom 𝑈 ∧ ∀𝑣𝐵𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑇𝐺) = (𝑈𝐺))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∃*wmo 2555  ∃!weu 2587  {cab 2735  ∀wral 3070  ∃wrex 3071  Vcvv 3409   ∪ cun 3858   ⊆ wss 3860  ifcif 4423  {csn 4525  ⟨cop 4531   class class class wbr 5036   ↦ cmpt 5116  dom cdm 5528   ↾ cres 5530  suc csuc 6176  ℩cio 6297  ‘cfv 6340  ℩crio 7113  1oc1o 8111   No csur 33440
 Copyright terms: Public domain W3C validator