Theorem cofcut1 28124

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 1219	. . 3 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐶 <<s {(𝐴 |s 𝐵)})
2		simp3r 1220	. . 3 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → {(𝐴 |s 𝐵)} <<s 𝐷)
3		simp1 1153	. . . . . 6 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐴 <<s 𝐵)
4		cutbday 27988	. . . . . 6 ⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
5	3, 4	syl 18	. . . . 5 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
6		sltsex1 27967	. . . . . . . . . . . . 13 ⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
7	3, 6	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐴 ∈ V)
8	7	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐴 ∈ V)
9		sltsss1 27969	. . . . . . . . . . . . 13 ⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No )
10	3, 9	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐴 ⊆ No )
11	10	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐴 ⊆ No )
12	8, 11	elpwd 4567	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐴 ∈ 𝒫 No )
13		simpl2l 1244	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦)
14	13	adantr 485	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦)
15		simpr 489	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐶 <<s {𝑡})
16		cofslts 28122	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ 𝐶 <<s {𝑡}) → 𝐴 <<s {𝑡})
17	12, 14, 15, 16	syl3anc 1397	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐴 <<s {𝑡})
18	17	ex 417	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) → (𝐶 <<s {𝑡} → 𝐴 <<s {𝑡}))
19		sltsex2 27968	. . . . . . . . . . . . 13 ⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
20	3, 19	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐵 ∈ V)
21	20	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → 𝐵 ∈ V)
22		sltsss2 27970	. . . . . . . . . . . . 13 ⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )
23	3, 22	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐵 ⊆ No )
24	23	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → 𝐵 ⊆ No )
25	21, 24	elpwd 4567	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → 𝐵 ∈ 𝒫 No )
26		simpl2r 1245	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧)
27	26	adantr 485	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧)
28		simpr 489	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → {𝑡} <<s 𝐷)
29		coinitslts 28123	. . . . . . . . . 10 ⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ∧ {𝑡} <<s 𝐷) → {𝑡} <<s 𝐵)
30	25, 27, 28, 29	syl3anc 1397	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → {𝑡} <<s 𝐵)
31	30	ex 417	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) → ({𝑡} <<s 𝐷 → {𝑡} <<s 𝐵))
32	18, 31	anim12d 620	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) → ((𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷) → (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)))
33	32	ss2rabdv 4028	. . . . . 6 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
34		imass2 6103	. . . . . 6 ⊢ ({𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} → ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) ⊆ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
35		intss 4933	. . . . . 6 ⊢ (( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) ⊆ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
36	33, 34, 35	3syl 19	. . . . 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 27952	. . . . . 6 ⊢ bday Fn No
39		ssrab2 4033	. . . . . 6 ⊢ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ No
40		sneq 4598	. . . . . . . . 9 ⊢ (𝑡 = (𝐴 |s 𝐵) → {𝑡} = {(𝐴 |s 𝐵)})
41	40	breq2d 5120	. . . . . . . 8 ⊢ (𝑡 = (𝐴 |s 𝐵) → (𝐶 <<s {𝑡} ↔ 𝐶 <<s {(𝐴 |s 𝐵)}))
42	40	breq1d 5118	. . . . . . . 8 ⊢ (𝑡 = (𝐴 |s 𝐵) → ({𝑡} <<s 𝐷 ↔ {(𝐴 |s 𝐵)} <<s 𝐷))
43	41, 42	anbi12d 643	. . . . . . 7 ⊢ (𝑡 = (𝐴 |s 𝐵) → ((𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷) ↔ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)))
44	3	cutscld 27987	. . . . . . 7 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) ∈ No )
45		simp3 1155	. . . . . . 7 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷))
46	43, 44, 45	elrabd 3651	. . . . . 6 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) ∈ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)})
47		fnfvima 7231	. . . . . 6 ⊢ (( bday Fn No ∧ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ No ∧ (𝐴 |s 𝐵) ∈ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) → ( bday ‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
48	38, 39, 46, 47	mp3an12i 1493	. . . . 5 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday ‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
49		intss1 4927	. . . . 5 ⊢ (( bday ‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) ⊆ ( bday ‘(𝐴 |s 𝐵)))
50	48, 49	syl 18	. . . 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 7445	. . . . . . 7 ⊢ (𝐴 |s 𝐵) ∈ V
53	52	snnz 4741	. . . . . 6 ⊢ {(𝐴 |s 𝐵)} ≠ ∅
54		sltstr 27991	. . . . . 6 ⊢ ((𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷 ∧ {(𝐴 |s 𝐵)} ≠ ∅) → 𝐶 <<s 𝐷)
55	53, 54	mp3an3 1478	. . . . 5 ⊢ ((𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → 𝐶 <<s 𝐷)
56	55	3ad2ant3 1152	. . . 4 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐶 <<s 𝐷)
57		eqcuts 27989	. . . 4 ⊢ ((𝐶 <<s 𝐷 ∧ (𝐴 |s 𝐵) ∈ No ) → ((𝐶 |s 𝐷) = (𝐴 |s 𝐵) ↔ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷 ∧ ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))))
58	56, 44, 57	syl2anc 595	. . 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 1360	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐶 |s 𝐷) = (𝐴 |s 𝐵))
60	59	eqcomd 2768	1 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) = (𝐶 |s 𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1102   = wceq 1569   ∈ wcel 2142   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  {crab 3415  Vcvv 3454   ⊆ wss 3904  ∅c0 4285  𝒫 cpw 4561  {csn 4588  ∩ cint 4911   class class class wbr 5108   “ cima 5663   Fn wfn 6531  ‘cfv 6536  (class class class)co 7412   No csur 27815   bday cbday 27817   ≤s cles 27919   <<s cslts 27961   |s ccuts 27963

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4595  df-uni 4872  df-int 4912  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-ord 6363  df-on 6364  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1o 8451  df-2o 8452  df-no 27818  df-lts 27819  df-bday 27820  df-les 27920  df-slts 27962  df-cuts 27964

This theorem is used by:  cofcut1d  28125  cofcut2  28126