Description: Strong axiom of replacement (universal closure of ax-rep ) from the axioms of separation and replacement as written in the theorem's hypotheses.
The statement does not require a nonempty universe; most of the proof does not either, except for the use of 19.8a , which could be removed by reworking the proof, since it is applied in a subexpression bound by the variable it introduces. Proof modifications should not introduce steps relying on a nonempty universe, like alrimiv . (Contributed by BJ, 14-Mar-2026) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bj-axreprepsep.axsep | ⊢ ∀ 𝑥 ∃ 𝑠 ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) | |
| bj-axreprepsep.axrep | ⊢ ∀ 𝑠 ( ∀ 𝑦 ∈ 𝑠 ∃! 𝑧 𝜑 → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) | ||
| Assertion | bj-axreprepsep | ⊢ ∀ 𝑥 ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-axreprepsep.axsep | ⊢ ∀ 𝑥 ∃ 𝑠 ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) | |
| 2 | bj-axreprepsep.axrep | ⊢ ∀ 𝑠 ( ∀ 𝑦 ∈ 𝑠 ∃! 𝑧 𝜑 → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) | |
| 3 | 19.42v | ⊢ ( ∃ 𝑠 ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) ↔ ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∃ 𝑠 ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) ) | |
| 4 | bianir | ⊢ ( ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ∧ ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ) | |
| 5 | 4 | ax-gen | ⊢ ∀ 𝑠 ( ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ∧ ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ) |
| 6 | pm3.43 | ⊢ ( ( ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) ) → ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ∧ ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) ) ) | |
| 7 | df-ral | ⊢ ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃* 𝑧 𝜑 ) ) | |
| 8 | bicom1 | ⊢ ( ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ↔ 𝑦 ∈ 𝑠 ) ) | |
| 9 | 8 | biimprcd | ⊢ ( 𝑦 ∈ 𝑠 → ( ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) |
| 10 | df-eu | ⊢ ( ∃! 𝑧 𝜑 ↔ ( ∃ 𝑧 𝜑 ∧ ∃* 𝑧 𝜑 ) ) | |
| 11 | 10 | simplbi2com | ⊢ ( ∃* 𝑧 𝜑 → ( ∃ 𝑧 𝜑 → ∃! 𝑧 𝜑 ) ) |
| 12 | 11 | imim2i | ⊢ ( ( 𝑦 ∈ 𝑥 → ∃* 𝑧 𝜑 ) → ( 𝑦 ∈ 𝑥 → ( ∃ 𝑧 𝜑 → ∃! 𝑧 𝜑 ) ) ) |
| 13 | 12 | impd | ⊢ ( ( 𝑦 ∈ 𝑥 → ∃* 𝑧 𝜑 ) → ( ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) → ∃! 𝑧 𝜑 ) ) |
| 14 | 13 | com12 | ⊢ ( ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) → ( ( 𝑦 ∈ 𝑥 → ∃* 𝑧 𝜑 ) → ∃! 𝑧 𝜑 ) ) |
| 15 | 9 14 | syl6 | ⊢ ( 𝑦 ∈ 𝑠 → ( ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( ( 𝑦 ∈ 𝑥 → ∃* 𝑧 𝜑 ) → ∃! 𝑧 𝜑 ) ) ) |
| 16 | 15 | impd | ⊢ ( 𝑦 ∈ 𝑠 → ( ( ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ∧ ( 𝑦 ∈ 𝑥 → ∃* 𝑧 𝜑 ) ) → ∃! 𝑧 𝜑 ) ) |
| 17 | 16 | com12 | ⊢ ( ( ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ∧ ( 𝑦 ∈ 𝑥 → ∃* 𝑧 𝜑 ) ) → ( 𝑦 ∈ 𝑠 → ∃! 𝑧 𝜑 ) ) |
| 18 | 17 | ancoms | ⊢ ( ( ( 𝑦 ∈ 𝑥 → ∃* 𝑧 𝜑 ) ∧ ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ( 𝑦 ∈ 𝑠 → ∃! 𝑧 𝜑 ) ) |
| 19 | 18 | alanimi | ⊢ ( ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃* 𝑧 𝜑 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∀ 𝑦 ( 𝑦 ∈ 𝑠 → ∃! 𝑧 𝜑 ) ) |
| 20 | 7 19 | sylanb | ⊢ ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∀ 𝑦 ( 𝑦 ∈ 𝑠 → ∃! 𝑧 𝜑 ) ) |
| 21 | 20 | ralrid | ⊢ ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∀ 𝑦 ∈ 𝑠 ∃! 𝑧 𝜑 ) |
| 22 | 21 | ax-gen | ⊢ ∀ 𝑠 ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∀ 𝑦 ∈ 𝑠 ∃! 𝑧 𝜑 ) |
| 23 | 2 22 | barbara | ⊢ ∀ 𝑠 ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) |
| 24 | nfv | ⊢ Ⅎ 𝑧 𝑦 ∈ 𝑠 | |
| 25 | nfv | ⊢ Ⅎ 𝑧 𝑦 ∈ 𝑥 | |
| 26 | nfe1 | ⊢ Ⅎ 𝑧 ∃ 𝑧 𝜑 | |
| 27 | 25 26 | nfan | ⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) |
| 28 | 24 27 | nfbi | ⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) |
| 29 | 28 | nfal | ⊢ Ⅎ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) |
| 30 | 19.8a | ⊢ ( 𝜑 → ∃ 𝑧 𝜑 ) | |
| 31 | biimpr | ⊢ ( ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) → 𝑦 ∈ 𝑠 ) ) | |
| 32 | 30 31 | sylan2i | ⊢ ( ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → 𝑦 ∈ 𝑠 ) ) |
| 33 | simpr | ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → 𝜑 ) | |
| 34 | 32 33 | jca2 | ⊢ ( ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) → ( 𝑦 ∈ 𝑠 ∧ 𝜑 ) ) ) |
| 35 | bj-bisimpl | ⊢ ( ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( 𝑦 ∈ 𝑠 → 𝑦 ∈ 𝑥 ) ) | |
| 36 | 35 | anim1d | ⊢ ( ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( ( 𝑦 ∈ 𝑠 ∧ 𝜑 ) → ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ) ) |
| 37 | 34 36 | impbid | ⊢ ( ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ↔ ( 𝑦 ∈ 𝑠 ∧ 𝜑 ) ) ) |
| 38 | 37 | alexbii | ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑠 ∧ 𝜑 ) ) ) |
| 39 | df-rex | ⊢ ( ∃ 𝑦 ∈ 𝑥 𝜑 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ 𝜑 ) ) | |
| 40 | df-rex | ⊢ ( ∃ 𝑦 ∈ 𝑠 𝜑 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑠 ∧ 𝜑 ) ) | |
| 41 | 38 39 40 | 3bitr4g | ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( ∃ 𝑦 ∈ 𝑥 𝜑 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) |
| 42 | 41 | bibi2d | ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) |
| 43 | 29 42 | albid | ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) |
| 44 | 43 | exbidv | ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) |
| 45 | 44 | adantl | ⊢ ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) |
| 46 | 45 | ax-gen | ⊢ ∀ 𝑠 ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) |
| 47 | 19.26 | ⊢ ( ∀ 𝑠 ( ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) ) ↔ ( ∀ 𝑠 ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ∧ ∀ 𝑠 ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) ) ) | |
| 48 | 23 46 47 | mpbir2an | ⊢ ∀ 𝑠 ( ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ∧ ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) ) |
| 49 | 6 48 | bj-alimii | ⊢ ∀ 𝑠 ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ∧ ( ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ↔ ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑠 𝜑 ) ) ) ) |
| 50 | 5 49 | barbara | ⊢ ∀ 𝑠 ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ) |
| 51 | exim | ⊢ ( ∀ 𝑠 ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ) → ( ∃ 𝑠 ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∃ 𝑠 ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ) ) | |
| 52 | 50 51 | ax-mp | ⊢ ( ∃ 𝑠 ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∃ 𝑠 ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ) |
| 53 | 3 52 | sylbir | ⊢ ( ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 ∧ ∃ 𝑠 ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) ) → ∃ 𝑠 ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ) |
| 54 | 53 | ex | ⊢ ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 → ( ∃ 𝑠 ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ∃ 𝑠 ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ) ) |
| 55 | ax5e | ⊢ ( ∃ 𝑠 ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ) | |
| 56 | 54 55 | syl6 | ⊢ ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 → ( ∃ 𝑠 ∀ 𝑦 ( 𝑦 ∈ 𝑠 ↔ ( 𝑦 ∈ 𝑥 ∧ ∃ 𝑧 𝜑 ) ) → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ) ) |
| 57 | 56 1 | bj-almpig | ⊢ ∀ 𝑥 ( ∀ 𝑦 ∈ 𝑥 ∃* 𝑧 𝜑 → ∃ 𝑡 ∀ 𝑧 ( 𝑧 ∈ 𝑡 ↔ ∃ 𝑦 ∈ 𝑥 𝜑 ) ) |