Theorem cofcut1 27933

Description: If 𝐶 is cofinal with 𝐴 and 𝐷 is coinitial with 𝐵 and the cut of 𝐴 and 𝐵 lies between 𝐶 and 𝐷, then the cut of 𝐶 and 𝐷 is equal to the cut of 𝐴 and 𝐵. Theorem 2.6 of [Gonshor] p. 10. (Contributed by Scott Fenton, 25-Sep-2024.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑧,𝐵   𝑥,𝐶,𝑦   𝑤,𝐷,𝑧

Allowed substitution hints:   𝐴(𝑦,𝑧,𝑤)   𝐵(𝑥,𝑦,𝑤)   𝐶(𝑧,𝑤)   𝐷(𝑥,𝑦)

Proof of Theorem cofcut1

Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp3l 1203	. . 3 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐶 <<s {(𝐴 |s 𝐵)})
2		simp3r 1204	. . 3 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → {(𝐴 |s 𝐵)} <<s 𝐷)
3		simp1 1137	. . . . . 6 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐴 <<s 𝐵)
4		cutbday 27797	. . . . . 6 ⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
5	3, 4	syl 17	. . . . 5 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
6		sltsex1 27776	. . . . . . . . . . . . 13 ⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
7	3, 6	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐴 ∈ V)
8	7	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐴 ∈ V)
9		sltsss1 27778	. . . . . . . . . . . . 13 ⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No )
10	3, 9	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐴 ⊆ No )
11	10	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐴 ⊆ No )
12	8, 11	elpwd 4562	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐴 ∈ 𝒫 No )
13		simpl2l 1228	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦)
14	13	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦)
15		simpr 484	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐶 <<s {𝑡})
16		cofslts 27931	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ 𝐶 <<s {𝑡}) → 𝐴 <<s {𝑡})
17	12, 14, 15, 16	syl3anc 1374	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐴 <<s {𝑡})
18	17	ex 412	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) → (𝐶 <<s {𝑡} → 𝐴 <<s {𝑡}))
19		sltsex2 27777	. . . . . . . . . . . . 13 ⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
20	3, 19	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐵 ∈ V)
21	20	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → 𝐵 ∈ V)
22		sltsss2 27779	. . . . . . . . . . . . 13 ⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )
23	3, 22	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐵 ⊆ No )
24	23	ad2antrr 727	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → 𝐵 ⊆ No )
25	21, 24	elpwd 4562	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → 𝐵 ∈ 𝒫 No )
26		simpl2r 1229	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧)
27	26	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧)
28		simpr 484	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → {𝑡} <<s 𝐷)
29		coinitslts 27932	. . . . . . . . . 10 ⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ∧ {𝑡} <<s 𝐷) → {𝑡} <<s 𝐵)
30	25, 27, 28, 29	syl3anc 1374	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → {𝑡} <<s 𝐵)
31	30	ex 412	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) → ({𝑡} <<s 𝐷 → {𝑡} <<s 𝐵))
32	18, 31	anim12d 610	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) → ((𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷) → (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)))
33	32	ss2rabdv 4029	. . . . . 6 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
34		imass2 6071	. . . . . 6 ⊢ ({𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} → ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) ⊆ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
35		intss 4926	. . . . . 6 ⊢ (( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) ⊆ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
36	33, 34, 35	3syl 18	. . . . 5 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
37	5, 36	eqsstrd 3970	. . . 4 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
38		bdayfn 27762	. . . . . 6 ⊢ bday Fn No
39		ssrab2 4034	. . . . . 6 ⊢ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ No
40		sneq 4592	. . . . . . . . 9 ⊢ (𝑡 = (𝐴 |s 𝐵) → {𝑡} = {(𝐴 |s 𝐵)})
41	40	breq2d 5112	. . . . . . . 8 ⊢ (𝑡 = (𝐴 |s 𝐵) → (𝐶 <<s {𝑡} ↔ 𝐶 <<s {(𝐴 |s 𝐵)}))
42	40	breq1d 5110	. . . . . . . 8 ⊢ (𝑡 = (𝐴 |s 𝐵) → ({𝑡} <<s 𝐷 ↔ {(𝐴 |s 𝐵)} <<s 𝐷))
43	41, 42	anbi12d 633	. . . . . . 7 ⊢ (𝑡 = (𝐴 |s 𝐵) → ((𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷) ↔ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)))
44	3	cutscld 27796	. . . . . . 7 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) ∈ No )
45		simp3 1139	. . . . . . 7 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷))
46	43, 44, 45	elrabd 3650	. . . . . 6 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) ∈ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)})
47		fnfvima 7191	. . . . . 6 ⊢ (( bday Fn No ∧ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ No ∧ (𝐴 |s 𝐵) ∈ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) → ( bday ‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
48	38, 39, 46, 47	mp3an12i 1468	. . . . 5 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday ‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
49		intss1 4920	. . . . 5 ⊢ (( bday ‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) ⊆ ( bday ‘(𝐴 |s 𝐵)))
50	48, 49	syl 17	. . . 4 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) ⊆ ( bday ‘(𝐴 |s 𝐵)))
51	37, 50	eqssd 3953	. . 3 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
52		ovex 7403	. . . . . . 7 ⊢ (𝐴 |s 𝐵) ∈ V
53	52	snnz 4735	. . . . . 6 ⊢ {(𝐴 |s 𝐵)} ≠ ∅
54		sltstr 27800	. . . . . 6 ⊢ ((𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷 ∧ {(𝐴 |s 𝐵)} ≠ ∅) → 𝐶 <<s 𝐷)
55	53, 54	mp3an3 1453	. . . . 5 ⊢ ((𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → 𝐶 <<s 𝐷)
56	55	3ad2ant3 1136	. . . 4 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐶 <<s 𝐷)
57		eqcuts 27798	. . . 4 ⊢ ((𝐶 <<s 𝐷 ∧ (𝐴 |s 𝐵) ∈ No ) → ((𝐶 |s 𝐷) = (𝐴 |s 𝐵) ↔ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷 ∧ ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))))
58	56, 44, 57	syl2anc 585	. . 3 ⊢ ((𝐴 <<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 1344	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐶 |s 𝐷) = (𝐴 |s 𝐵))
60	59	eqcomd 2743	1 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) = (𝐶 |s 𝐷))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442   ⊆ wss 3903  ∅c0 4287  𝒫 cpw 4556  {csn 4582  ∩ cint 4904   class class class wbr 5100   “ cima 5637   Fn wfn 6497  ‘cfv 6502  (class class class)co 7370   No csur 27624   bday cbday 27626   ≤s cles 27729   <<s cslts 27770   |s ccuts 27772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4905  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-ord 6330  df-on 6331  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-1o 8409  df-2o 8410  df-no 27627  df-lts 27628  df-bday 27629  df-les 27730  df-slts 27771  df-cuts 27773

This theorem is referenced by:  cofcut1d  27934  cofcut2  27935