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

Theorem eqscut2 33587
 Description: Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024.)
Assertion
Ref Expression
eqscut2 ((𝐿 <<s 𝑅𝑋 No ) → ((𝐿 |s 𝑅) = 𝑋 ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ∀𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦)))))
Distinct variable groups:   𝑦,𝐿   𝑦,𝑅   𝑦,𝑋

Proof of Theorem eqscut2
Dummy variables 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqscut 33586 . 2 ((𝐿 <<s 𝑅𝑋 No ) → ((𝐿 |s 𝑅) = 𝑋 ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday 𝑋) = ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}))))
2 eqss 3909 . . . . 5 (( bday 𝑋) = ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ (( bday 𝑋) ⊆ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ∧ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ⊆ ( bday 𝑋)))
3 sneq 4535 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → {𝑥} = {𝑋})
43breq2d 5047 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (𝐿 <<s {𝑥} ↔ 𝐿 <<s {𝑋}))
53breq1d 5045 . . . . . . . . . . . 12 (𝑥 = 𝑋 → ({𝑥} <<s 𝑅 ↔ {𝑋} <<s 𝑅))
64, 5anbi12d 633 . . . . . . . . . . 11 (𝑥 = 𝑋 → ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)))
76elrab3 3605 . . . . . . . . . 10 (𝑋 No → (𝑋 ∈ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)))
87adantl 485 . . . . . . . . 9 ((𝐿 <<s 𝑅𝑋 No ) → (𝑋 ∈ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)))
98biimpar 481 . . . . . . . 8 (((𝐿 <<s 𝑅𝑋 No ) ∧ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)) → 𝑋 ∈ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})
10 bdayfn 33557 . . . . . . . . 9 bday Fn No
11 ssrab2 3986 . . . . . . . . 9 {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} ⊆ No
12 fnfvima 6992 . . . . . . . . 9 (( bday Fn No ∧ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} ⊆ No 𝑋 ∈ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) → ( bday 𝑋) ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}))
1310, 11, 12mp3an12 1448 . . . . . . . 8 (𝑋 ∈ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} → ( bday 𝑋) ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}))
14 intss1 4856 . . . . . . . 8 (( bday 𝑋) ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) → ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ⊆ ( bday 𝑋))
159, 13, 143syl 18 . . . . . . 7 (((𝐿 <<s 𝑅𝑋 No ) ∧ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)) → ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ⊆ ( bday 𝑋))
1615biantrud 535 . . . . . 6 (((𝐿 <<s 𝑅𝑋 No ) ∧ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)) → (( bday 𝑋) ⊆ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ (( bday 𝑋) ⊆ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ∧ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ⊆ ( bday 𝑋))))
17 ssint 4857 . . . . . . 7 (( bday 𝑋) ⊆ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ ∀𝑧 ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})( bday 𝑋) ⊆ 𝑧)
18 fvelimab 6729 . . . . . . . . . . . . . 14 (( bday Fn No ∧ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} ⊆ No ) → (𝑧 ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ ∃𝑦 ∈ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} ( bday 𝑦) = 𝑧))
1910, 11, 18mp2an 691 . . . . . . . . . . . . 13 (𝑧 ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ ∃𝑦 ∈ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} ( bday 𝑦) = 𝑧)
20 sneq 4535 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → {𝑥} = {𝑦})
2120breq2d 5047 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝐿 <<s {𝑥} ↔ 𝐿 <<s {𝑦}))
2220breq1d 5045 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ({𝑥} <<s 𝑅 ↔ {𝑦} <<s 𝑅))
2321, 22anbi12d 633 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ↔ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)))
2423rexrab 3612 . . . . . . . . . . . . 13 (∃𝑦 ∈ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)} ( bday 𝑦) = 𝑧 ↔ ∃𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday 𝑦) = 𝑧))
2519, 24bitri 278 . . . . . . . . . . . 12 (𝑧 ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ ∃𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday 𝑦) = 𝑧))
2625imbi1i 353 . . . . . . . . . . 11 ((𝑧 ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) → ( bday 𝑋) ⊆ 𝑧) ↔ (∃𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday 𝑦) = 𝑧) → ( bday 𝑋) ⊆ 𝑧))
27 r19.23v 3203 . . . . . . . . . . 11 (∀𝑦 No (((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday 𝑦) = 𝑧) → ( bday 𝑋) ⊆ 𝑧) ↔ (∃𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday 𝑦) = 𝑧) → ( bday 𝑋) ⊆ 𝑧))
28 eqcom 2765 . . . . . . . . . . . . . . 15 (( bday 𝑦) = 𝑧𝑧 = ( bday 𝑦))
2928anbi1ci 628 . . . . . . . . . . . . . 14 (((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday 𝑦) = 𝑧) ↔ (𝑧 = ( bday 𝑦) ∧ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)))
3029imbi1i 353 . . . . . . . . . . . . 13 ((((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday 𝑦) = 𝑧) → ( bday 𝑋) ⊆ 𝑧) ↔ ((𝑧 = ( bday 𝑦) ∧ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)) → ( bday 𝑋) ⊆ 𝑧))
31 impexp 454 . . . . . . . . . . . . 13 (((𝑧 = ( bday 𝑦) ∧ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)) → ( bday 𝑋) ⊆ 𝑧) ↔ (𝑧 = ( bday 𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ 𝑧)))
3230, 31bitri 278 . . . . . . . . . . . 12 ((((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday 𝑦) = 𝑧) → ( bday 𝑋) ⊆ 𝑧) ↔ (𝑧 = ( bday 𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ 𝑧)))
3332ralbii 3097 . . . . . . . . . . 11 (∀𝑦 No (((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) ∧ ( bday 𝑦) = 𝑧) → ( bday 𝑋) ⊆ 𝑧) ↔ ∀𝑦 No (𝑧 = ( bday 𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ 𝑧)))
3426, 27, 333bitr2i 302 . . . . . . . . . 10 ((𝑧 ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) → ( bday 𝑋) ⊆ 𝑧) ↔ ∀𝑦 No (𝑧 = ( bday 𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ 𝑧)))
3534albii 1821 . . . . . . . . 9 (∀𝑧(𝑧 ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) → ( bday 𝑋) ⊆ 𝑧) ↔ ∀𝑧𝑦 No (𝑧 = ( bday 𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ 𝑧)))
36 df-ral 3075 . . . . . . . . 9 (∀𝑧 ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})( bday 𝑋) ⊆ 𝑧 ↔ ∀𝑧(𝑧 ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) → ( bday 𝑋) ⊆ 𝑧))
37 ralcom4 3162 . . . . . . . . 9 (∀𝑦 No 𝑧(𝑧 = ( bday 𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ 𝑧)) ↔ ∀𝑧𝑦 No (𝑧 = ( bday 𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ 𝑧)))
3835, 36, 373bitr4i 306 . . . . . . . 8 (∀𝑧 ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})( bday 𝑋) ⊆ 𝑧 ↔ ∀𝑦 No 𝑧(𝑧 = ( bday 𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ 𝑧)))
39 fvex 6675 . . . . . . . . . 10 ( bday 𝑦) ∈ V
40 sseq2 3920 . . . . . . . . . . 11 (𝑧 = ( bday 𝑦) → (( bday 𝑋) ⊆ 𝑧 ↔ ( bday 𝑋) ⊆ ( bday 𝑦)))
4140imbi2d 344 . . . . . . . . . 10 (𝑧 = ( bday 𝑦) → (((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ 𝑧) ↔ ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦))))
4239, 41ceqsalv 3448 . . . . . . . . 9 (∀𝑧(𝑧 = ( bday 𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ 𝑧)) ↔ ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦)))
4342ralbii 3097 . . . . . . . 8 (∀𝑦 No 𝑧(𝑧 = ( bday 𝑦) → ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ 𝑧)) ↔ ∀𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦)))
4438, 43bitri 278 . . . . . . 7 (∀𝑧 ∈ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})( bday 𝑋) ⊆ 𝑧 ↔ ∀𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦)))
4517, 44bitri 278 . . . . . 6 (( bday 𝑋) ⊆ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ ∀𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦)))
4616, 45bitr3di 289 . . . . 5 (((𝐿 <<s 𝑅𝑋 No ) ∧ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)) → ((( bday 𝑋) ⊆ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ∧ ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ⊆ ( bday 𝑋)) ↔ ∀𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦))))
472, 46syl5bb 286 . . . 4 (((𝐿 <<s 𝑅𝑋 No ) ∧ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅)) → (( bday 𝑋) = ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)}) ↔ ∀𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦))))
4847pm5.32da 582 . . 3 ((𝐿 <<s 𝑅𝑋 No ) → (((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅) ∧ ( bday 𝑋) = ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})) ↔ ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅) ∧ ∀𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦)))))
49 df-3an 1086 . . 3 ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday 𝑋) = ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})) ↔ ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅) ∧ ( bday 𝑋) = ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})))
50 df-3an 1086 . . 3 ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ∀𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦))) ↔ ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅) ∧ ∀𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦))))
5148, 49, 503bitr4g 317 . 2 ((𝐿 <<s 𝑅𝑋 No ) → ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday 𝑋) = ( bday “ {𝑥 No ∣ (𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅)})) ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ∀𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦)))))
521, 51bitrd 282 1 ((𝐿 <<s 𝑅𝑋 No ) → ((𝐿 |s 𝑅) = 𝑋 ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ∀𝑦 No ((𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅) → ( bday 𝑋) ⊆ ( bday 𝑦)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084  ∀wal 1536   = wceq 1538   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071  {crab 3074   ⊆ wss 3860  {csn 4525  ∩ cint 4841   class class class wbr 5035   “ cima 5530   Fn wfn 6334  ‘cfv 6339  (class class class)co 7155   No csur 33432   bday cbday 33434   <
 Copyright terms: Public domain W3C validator