Metamath Proof Explorer

Theorem cofcut1

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, 25-Sep-2024)

Ref Expression
Assertion cofcut1 ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) )

Proof

Step Hyp Ref Expression
1 simp3l ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → 𝐶 <<s { ( 𝐴 |s 𝐵 ) } )
2 simp3r ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → { ( 𝐴 |s 𝐵 ) } <<s 𝐷 )
3 simp1 ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → 𝐴 <<s 𝐵 )
4 scutbday ⊢ ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) )
5 3 4 syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) )
6 ssltex1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
7 3 6 syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → 𝐴 ∈ V )
8 7 ad2antrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s { 𝑡 } ) → 𝐴 ∈ V )
9 ssltss1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No )
10 3 9 syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → 𝐴 ⊆ No )
11 10 ad2antrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s { 𝑡 } ) → 𝐴 ⊆ No )
12 8 11 elpwd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s { 𝑡 } ) → 𝐴 ∈ 𝒫 No )
13 simpl2l ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 )
14 13 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s { 𝑡 } ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 )
15 simpr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s { 𝑡 } ) → 𝐶 <<s { 𝑡 } )
16 cofsslt ⊢ ( ( 𝐴 ∈ 𝒫 No ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ 𝐶 <<s { 𝑡 } ) → 𝐴 <<s { 𝑡 } )
17 12 14 15 16 syl3anc ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s { 𝑡 } ) → 𝐴 <<s { 𝑡 } )
18 17 ex ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) → ( 𝐶 <<s { 𝑡 } → 𝐴 <<s { 𝑡 } ) )
19 ssltex2 ⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ V )
20 3 19 syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → 𝐵 ∈ V )
21 20 ad2antrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) ∧ { 𝑡 } <<s 𝐷 ) → 𝐵 ∈ V )
22 ssltss2 ⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No )
23 3 22 syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → 𝐵 ⊆ No )
24 23 ad2antrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) ∧ { 𝑡 } <<s 𝐷 ) → 𝐵 ⊆ No )
25 21 24 elpwd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) ∧ { 𝑡 } <<s 𝐷 ) → 𝐵 ∈ 𝒫 No )
26 simpl2r ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 )
27 26 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) ∧ { 𝑡 } <<s 𝐷 ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 )
28 simpr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) ∧ { 𝑡 } <<s 𝐷 ) → { 𝑡 } <<s 𝐷 )
29 coinitsslt ⊢ ( ( 𝐵 ∈ 𝒫 No ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ∧ { 𝑡 } <<s 𝐷 ) → { 𝑡 } <<s 𝐵 )
30 25 27 28 29 syl3anc ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) ∧ { 𝑡 } <<s 𝐷 ) → { 𝑡 } <<s 𝐵 )
31 30 ex ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) → ( { 𝑡 } <<s 𝐷 → { 𝑡 } <<s 𝐵 ) )
32 18 31 anim12d ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) ∧ 𝑡 ∈ No ) → ( ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) → ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) ) )
33 32 ss2rabdv ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ⊆ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } )
34 imass2 ⊢ ( { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ⊆ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } → ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) ⊆ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) )
35 intss ⊢ ( ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) ⊆ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) → ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) ⊆ ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) )
36 33 34 35 3syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐴 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐵 ) } ) ⊆ ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) )
37 5 36 eqsstrd ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) )
38 bdayfn ⊢ bday Fn No
39 ssrab2 ⊢ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ⊆ No
40 sneq ⊢ ( 𝑡 = ( 𝐴 |s 𝐵 ) → { 𝑡 } = { ( 𝐴 |s 𝐵 ) } )
41 40 breq2d ⊢ ( 𝑡 = ( 𝐴 |s 𝐵 ) → ( 𝐶 <<s { 𝑡 } ↔ 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ) )
42 40 breq1d ⊢ ( 𝑡 = ( 𝐴 |s 𝐵 ) → ( { 𝑡 } <<s 𝐷 ↔ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) )
43 41 42 anbi12d ⊢ ( 𝑡 = ( 𝐴 |s 𝐵 ) → ( ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) ↔ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) )
44 3 scutcld ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( 𝐴 |s 𝐵 ) ∈ No )
45 simp3 ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) )
46 43 44 45 elrabd ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( 𝐴 |s 𝐵 ) ∈ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } )
47 fnfvima ⊢ ( ( bday Fn No ∧ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ⊆ No ∧ ( 𝐴 |s 𝐵 ) ∈ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) )
48 38 39 46 47 mp3an12i ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) )
49 intss1 ⊢ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) → ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) ⊆ ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
50 48 49 syl ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) ⊆ ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
51 37 50 eqssd ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) )
52 ovex ⊢ ( 𝐴 |s 𝐵 ) ∈ V
53 52 snnz ⊢ { ( 𝐴 |s 𝐵 ) } ≠ ∅
54 sslttr ⊢ ( ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ∧ { ( 𝐴 |s 𝐵 ) } ≠ ∅ ) → 𝐶 <<s 𝐷 )
55 53 54 mp3an3 ⊢ ( ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) → 𝐶 <<s 𝐷 )
56 55 3ad2ant3 ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → 𝐶 <<s 𝐷 )
57 eqscut ⊢ ( ( 𝐶 <<s 𝐷 ∧ ( 𝐴 |s 𝐵 ) ∈ No ) → ( ( 𝐶 |s 𝐷 ) = ( 𝐴 |s 𝐵 ) ↔ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) ) ) )
58 56 44 57 syl2anc ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( ( 𝐶 |s 𝐷 ) = ( 𝐴 |s 𝐵 ) ↔ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑡 ∈ No ∣ ( 𝐶 <<s { 𝑡 } ∧ { 𝑡 } <<s 𝐷 ) } ) ) ) )
59 1 2 51 58 mpbir3and ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( 𝐶 |s 𝐷 ) = ( 𝐴 |s 𝐵 ) )
60 59 eqcomd ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) )