Metamath Proof Explorer

Theorem regsfromsetind

Description: Derivation of ax-regs from mh-setind . (Contributed by Matthew House, 4-Mar-2026)

Ref Expression
Hypothesis regsfromsetind.1 ⊢ ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) → ¬ 𝜑 )
Assertion regsfromsetind ( ∃ 𝑥 𝜑 → ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )

Proof

Step Hyp Ref Expression
1 regsfromsetind.1 ⊢ ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) → ¬ 𝜑 )
2 nfia1 ⊢ Ⅎ 𝑥 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) )
3 2 nfal ⊢ Ⅎ 𝑥 ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) )
4 3 nfn ⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) )
5 1 con2i ⊢ ( 𝜑 → ¬ ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) )
6 4 5 exlimi ⊢ ( ∃ 𝑥 𝜑 → ¬ ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) )
7 exnalimn ⊢ ( ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) ↔ ¬ ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
8 nfv ⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 )
9 nfv ⊢ Ⅎ 𝑥 𝑧 ∈ 𝑦
10 nfna1 ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 )
11 9 10 nfim ⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) )
12 elequ1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) )
13 sbequ12 ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
14 sb6 ⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) )
15 13 14 bitrdi ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
16 15 notbid ⊢ ( 𝑥 = 𝑧 → ( ¬ 𝜑 ↔ ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
17 12 16 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) ↔ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
18 8 11 17 cbvalv1 ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
19 alinexa ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ↔ ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
20 sbalex ⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
21 19 20 xchbinx ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ↔ ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
22 18 21 imbi12i ⊢ ( ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) ↔ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) → ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
23 con2b ⊢ ( ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) → ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
24 22 23 bitri ⊢ ( ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
25 24 albii ⊢ ( ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) ↔ ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
26 7 25 xchbinxr ⊢ ( ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) ↔ ¬ ∀ 𝑦 ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) )
27 6 26 sylibr ⊢ ( ∃ 𝑥 𝜑 → ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )