Metamath Proof Explorer

Theorem coiniss

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

Ref Expression
Hypotheses cofss.1 ⊢ φ → A ⊆ No
cofss.2 ⊢ φ → B ⊆ A
Assertion coiniss ⊢ φ → ∀ x ∈ B ∃ y ∈ A y ≤ s x

Proof

Step Hyp Ref Expression
1 cofss.1 ⊢ φ → A ⊆ No
2 cofss.2 ⊢ φ → B ⊆ A
3 2 sselda ⊢ φ ∧ z ∈ B → z ∈ A
4 2 1 sstrd ⊢ φ → B ⊆ No
5 4 sselda ⊢ φ ∧ z ∈ B → z ∈ No
6 lesid ⊢ z ∈ No → z ≤ s z
7 5 6 syl ⊢ φ ∧ z ∈ B → z ≤ s z
8 breq1 ⊢ y = z → y ≤ s z ↔ z ≤ s z
9 8 rspcev ⊢ z ∈ A ∧ z ≤ s z → ∃ y ∈ A y ≤ s z
10 3 7 9 syl2anc ⊢ φ ∧ z ∈ B → ∃ y ∈ A y ≤ s z
11 10 ralrimiva ⊢ φ → ∀ z ∈ B ∃ y ∈ A y ≤ s z
12 breq2 ⊢ x = z → y ≤ s x ↔ y ≤ s z
13 12 rexbidv ⊢ x = z → ∃ y ∈ A y ≤ s x ↔ ∃ y ∈ A y ≤ s z
14 13 cbvralvw ⊢ ∀ x ∈ B ∃ y ∈ A y ≤ s x ↔ ∀ z ∈ B ∃ y ∈ A y ≤ s z
15 11 14 sylibr ⊢ φ → ∀ x ∈ B ∃ y ∈ A y ≤ s x