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 𝐷 ) )