This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axunndlem1

Description: Lemma for the Axiom of Union with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jan-2002) (New usage is discouraged.)

Ref Expression
Assertion axunndlem1 ∃ 𝑥 ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 )

Proof

Step Hyp Ref Expression
1 en2lp ⊢ ¬ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 )
2 elequ2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧 ) )
3 2 anbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) ) )
4 1 3 mtbii ⊢ ( 𝑦 = 𝑧 → ¬ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) )
5 4 sps ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ¬ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) )
6 5 nexdv ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ¬ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) )
7 6 pm2.21d ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
8 7 axc4i ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
9 8 19.8ad ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
10 zfun ⊢ ∃ 𝑥 ∀ 𝑤 ( ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 )
11 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑦 𝑦 = 𝑧
12 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑧
13 nfvd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 𝑤 ∈ 𝑥 )
14 nfcvf ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 𝑧 )
15 14 nfcrd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 𝑥 ∈ 𝑧 )
16 13 15 nfand ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) )
17 12 16 nfexd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) )
18 17 13 nfimd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 ( ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) )
19 elequ1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
20 19 anbi1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) ) )
21 20 exbidv ⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) ↔ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) ) )
22 21 19 imbi12d ⊢ ( 𝑤 = 𝑦 → ( ( ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ↔ ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
23 22 a1i ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( 𝑤 = 𝑦 → ( ( ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ↔ ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) )
24 11 18 23 cbvald ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑤 ( ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ↔ ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
25 24 exbidv ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∃ 𝑥 ∀ 𝑤 ( ∃ 𝑥 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑤 ∈ 𝑥 ) ↔ ∃ 𝑥 ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
26 10 25 mpbii ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
27 9 26 pm2.61i ⊢ ∃ 𝑥 ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 )