Description: If C is cofinal with A and D is coinitial with B and the cut of A and B lies between C and D , then the cut of C and D is equal to the cut of A and B . Theorem 2.6 of Gonshor p. 10. (Contributed by Scott Fenton, 23-Jan-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cofcut1d.1 | âĒ ( ð â ðī <<s ðĩ ) | |
cofcut1d.2 | âĒ ( ð â â ðĨ â ðī â ðĶ â ðķ ðĨ âĪs ðĶ ) | ||
cofcut1d.3 | âĒ ( ð â â ð§ â ðĩ â ðĪ â ð· ðĪ âĪs ð§ ) | ||
cofcut1d.4 | âĒ ( ð â ðķ <<s { ( ðī |s ðĩ ) } ) | ||
cofcut1d.5 | âĒ ( ð â { ( ðī |s ðĩ ) } <<s ð· ) | ||
Assertion | cofcut1d | âĒ ( ð â ( ðī |s ðĩ ) = ( ðķ |s ð· ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cofcut1d.1 | âĒ ( ð â ðī <<s ðĩ ) | |
2 | cofcut1d.2 | âĒ ( ð â â ðĨ â ðī â ðĶ â ðķ ðĨ âĪs ðĶ ) | |
3 | cofcut1d.3 | âĒ ( ð â â ð§ â ðĩ â ðĪ â ð· ðĪ âĪs ð§ ) | |
4 | cofcut1d.4 | âĒ ( ð â ðķ <<s { ( ðī |s ðĩ ) } ) | |
5 | cofcut1d.5 | âĒ ( ð â { ( ðī |s ðĩ ) } <<s ð· ) | |
6 | cofcut1 | âĒ ( ( ðī <<s ðĩ â§ ( â ðĨ â ðī â ðĶ â ðķ ðĨ âĪs ðĶ â§ â ð§ â ðĩ â ðĪ â ð· ðĪ âĪs ð§ ) â§ ( ðķ <<s { ( ðī |s ðĩ ) } â§ { ( ðī |s ðĩ ) } <<s ð· ) ) â ( ðī |s ðĩ ) = ( ðķ |s ð· ) ) | |
7 | 1 2 3 4 5 6 | syl122anc | âĒ ( ð â ( ðī |s ðĩ ) = ( ðķ |s ð· ) ) |