Theorem coiniss

Description: Coinitiality for a subset. (Contributed by Scott Fenton, 13-Mar-2025)

	Ref	Expression
Hypotheses	cofss.1	⊢ ( 𝜑 → 𝐴 ⊆ No )
	cofss.2	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
Assertion	coiniss	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		cofss.1	⊢ ( 𝜑 → 𝐴 ⊆ No )
2		cofss.2	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
3	2	sselda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐴 )
4	2 1	sstrd	⊢ ( 𝜑 → 𝐵 ⊆ No )
5	4	sselda	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ No )
6		lesid	⊢ ( 𝑧 ∈ No → 𝑧 ≤s 𝑧 )
7	5 6	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ≤s 𝑧 )
8		breq1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 ≤s 𝑧 ↔ 𝑧 ≤s 𝑧 ) )
9	8	rspcev	⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ≤s 𝑧 ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑧 )
10	3 7 9	syl2anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑧 )
11	10	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑧 )
12		breq2	⊢ ( 𝑥 = 𝑧 → ( 𝑦 ≤s 𝑥 ↔ 𝑦 ≤s 𝑧 ) )
13	12	rexbidv	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ↔ ∃ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑧 ) )
14	13	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ↔ ∀ 𝑧 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑧 )
15	11 14	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 )