Theorem cofcut1 34017

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 1199	. . 3 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐶 <<s {(𝐴 |s 𝐵)})
2		simp3r 1200	. . 3 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → {(𝐴 |s 𝐵)} <<s 𝐷)
3		simp1 1134	. . . . . 6 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐴 <<s 𝐵)
4		scutbday 33925	. . . . . 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		ssltex1 33908	. . . . . . . . . . . . 13 ⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
7	3, 6	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐴 ∈ V)
8	7	ad2antrr 722	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐴 ∈ V)
9		ssltss1 33910	. . . . . . . . . . . . 13 ⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No )
10	3, 9	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐴 ⊆ No )
11	10	ad2antrr 722	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐴 ⊆ No )
12	8, 11	elpwd 4538	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ 𝐶 <<s {𝑡}) → 𝐴 ∈ 𝒫 No )
13		simpl2l 1224	. . . . . . . . . . 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		cofsslt 34015	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ 𝐶 <<s {𝑡}) → 𝐴 <<s {𝑡})
17	12, 14, 15, 16	syl3anc 1369	. . . . . . . . 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		ssltex2 33909	. . . . . . . . . . . . 13 ⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
20	3, 19	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐵 ∈ V)
21	20	ad2antrr 722	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → 𝐵 ∈ V)
22		ssltss2 33911	. . . . . . . . . . . . 13 ⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )
23	3, 22	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐵 ⊆ No )
24	23	ad2antrr 722	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → 𝐵 ⊆ No )
25	21, 24	elpwd 4538	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) ∧ {𝑡} <<s 𝐷) → 𝐵 ∈ 𝒫 No )
26		simpl2r 1225	. . . . . . . . . . 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		coinitsslt 34016	. . . . . . . . . 10 ⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ∧ {𝑡} <<s 𝐷) → {𝑡} <<s 𝐵)
30	25, 27, 28, 29	syl3anc 1369	. . . . . . . . 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 608	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) ∧ 𝑡 ∈ No ) → ((𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷) → (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)))
33	32	ss2rabdv 4005	. . . . . 6 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
34		imass2 5999	. . . . . 6 ⊢ ({𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} → ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) ⊆ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
35		intss 4897	. . . . . 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 3955	. . . 4 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
38		bdayfn 33895	. . . . . 6 ⊢ bday Fn No
39		ssrab2 4009	. . . . . 6 ⊢ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ No
40		sneq 4568	. . . . . . . . 9 ⊢ (𝑡 = (𝐴 |s 𝐵) → {𝑡} = {(𝐴 |s 𝐵)})
41	40	breq2d 5082	. . . . . . . 8 ⊢ (𝑡 = (𝐴 |s 𝐵) → (𝐶 <<s {𝑡} ↔ 𝐶 <<s {(𝐴 |s 𝐵)}))
42	40	breq1d 5080	. . . . . . . 8 ⊢ (𝑡 = (𝐴 |s 𝐵) → ({𝑡} <<s 𝐷 ↔ {(𝐴 |s 𝐵)} <<s 𝐷))
43	41, 42	anbi12d 630	. . . . . . 7 ⊢ (𝑡 = (𝐴 |s 𝐵) → ((𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷) ↔ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)))
44	3	scutcld 33924	. . . . . . 7 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) ∈ No )
45		simp3 1136	. . . . . . 7 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷))
46	43, 44, 45	elrabd 3619	. . . . . 6 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) ∈ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)})
47		fnfvima 7091	. . . . . 6 ⊢ (( bday Fn No ∧ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)} ⊆ No ∧ (𝐴 |s 𝐵) ∈ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}) → ( bday ‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
48	38, 39, 46, 47	mp3an12i 1463	. . . . 5 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday ‘(𝐴 |s 𝐵)) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
49		intss1 4891	. . . . 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 3934	. . 3 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))
52		ovex 7288	. . . . . . 7 ⊢ (𝐴 |s 𝐵) ∈ V
53	52	snnz 4709	. . . . . 6 ⊢ {(𝐴 |s 𝐵)} ≠ ∅
54		sslttr 33928	. . . . . 6 ⊢ ((𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷 ∧ {(𝐴 |s 𝐵)} ≠ ∅) → 𝐶 <<s 𝐷)
55	53, 54	mp3an3 1448	. . . . 5 ⊢ ((𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷) → 𝐶 <<s 𝐷)
56	55	3ad2ant3 1133	. . . 4 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → 𝐶 <<s 𝐷)
57		eqscut 33926	. . . 4 ⊢ ((𝐶 <<s 𝐷 ∧ (𝐴 |s 𝐵) ∈ No ) → ((𝐶 |s 𝐷) = (𝐴 |s 𝐵) ↔ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷 ∧ ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐶 <<s {𝑡} ∧ {𝑡} <<s 𝐷)}))))
58	56, 44, 57	syl2anc 583	. . 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 1340	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐶 |s 𝐷) = (𝐴 |s 𝐵))
60	59	eqcomd 2744	1 ⊢ ((𝐴 <<s 𝐵 ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) ∧ (𝐶 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐷)) → (𝐴 |s 𝐵) = (𝐶 |s 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  {crab 3067  Vcvv 3422   ⊆ wss 3883  ∅c0 4253  𝒫 cpw 4530  {csn 4558  ∩ cint 4876   class class class wbr 5070   “ cima 5583   Fn wfn 6413  ‘cfv 6418  (class class class)co 7255   No csur 33770   bday cbday 33772   ≤s csle 33874   <<s csslt 33902   |s cscut 33904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-ord 6254  df-on 6255  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-1o 8267  df-2o 8268  df-no 33773  df-slt 33774  df-bday 33775  df-sle 33875  df-sslt 33903  df-scut 33905

This theorem is referenced by:  cofcut2  34018