Metamath Proof Explorer

Theorem eqcuts

Description: Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion eqcuts ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ( ( 𝐿 |s 𝑅 ) = 𝑋 ↔ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 cutsval ⊢ ( 𝐿 <<s 𝑅 → ( 𝐿 |s 𝑅 ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) )
2 1 adantr ⊢ ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ( 𝐿 |s 𝑅 ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) )
3 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
4 3 breq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐿 <<s { 𝑥 } ↔ 𝐿 <<s { 𝑦 } ) )
5 3 breq1d ⊢ ( 𝑥 = 𝑦 → ( { 𝑥 } <<s 𝑅 ↔ { 𝑦 } <<s 𝑅 ) )
6 4 5 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ↔ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) ) )
7 6 riotarab ⊢ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) = ( ℩ 𝑥 ∈ No ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) )
8 2 7 eqtrdi ⊢ ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ( 𝐿 |s 𝑅 ) = ( ℩ 𝑥 ∈ No ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ) )
9 8 eqeq1d ⊢ ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ( ( 𝐿 |s 𝑅 ) = 𝑋 ↔ ( ℩ 𝑥 ∈ No ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ) = 𝑋 ) )
10 conway ⊢ ( 𝐿 <<s 𝑅 → ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) )
11 6 reurab ⊢ ( ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ↔ ∃! 𝑥 ∈ No ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) )
12 10 11 sylib ⊢ ( 𝐿 <<s 𝑅 → ∃! 𝑥 ∈ No ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) )
13 df-3an ⊢ ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ↔ ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) )
14 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
15 14 breq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐿 <<s { 𝑥 } ↔ 𝐿 <<s { 𝑋 } ) )
16 14 breq1d ⊢ ( 𝑥 = 𝑋 → ( { 𝑥 } <<s 𝑅 ↔ { 𝑋 } <<s 𝑅 ) )
17 fveqeq2 ⊢ ( 𝑥 = 𝑋 → ( ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ↔ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) )
18 15 16 17 3anbi123d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ↔ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ) )
19 13 18 bitr3id ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ↔ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ) )
20 19 riota2 ⊢ ( ( 𝑋 ∈ No ∧ ∃! 𝑥 ∈ No ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ) → ( ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ↔ ( ℩ 𝑥 ∈ No ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ) = 𝑋 ) )
21 20 ancoms ⊢ ( ( ∃! 𝑥 ∈ No ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ∧ 𝑋 ∈ No ) → ( ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ↔ ( ℩ 𝑥 ∈ No ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ) = 𝑋 ) )
22 12 21 sylan ⊢ ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ( ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ↔ ( ℩ 𝑥 ∈ No ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ∧ ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ) = 𝑋 ) )
23 9 22 bitr4d ⊢ ( ( 𝐿 <<s 𝑅 ∧ 𝑋 ∈ No ) → ( ( 𝐿 |s 𝑅 ) = 𝑋 ↔ ( 𝐿 <<s { 𝑋 } ∧ { 𝑋 } <<s 𝑅 ∧ ( bday ‘ 𝑋 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐿 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑅 ) } ) ) ) )