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

Metamath Proof Explorer

Theorem axunnd

Description: A version of 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 axunnd ∃ 𝑥 ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 )

Proof

Step Hyp Ref Expression
1 axunndlem1 ⊢ ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 )
2 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
3 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑧
4 2 3 nfan ⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
5 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
6 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑧
7 5 6 nfan ⊢ Ⅎ 𝑦 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
8 nfv ⊢ Ⅎ 𝑤 ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 )
9 nfcvf ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 )
10 9 adantr ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑦 )
11 nfcvd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑤 )
12 10 11 nfeld ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑦 ∈ 𝑤 )
13 nfcvf ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 𝑧 )
14 13 adantl ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑧 )
15 11 14 nfeld ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑤 ∈ 𝑧 )
16 12 15 nfand ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) )
17 8 16 nfexd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∃ 𝑤 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) )
18 17 12 nfimd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ( ∃ 𝑤 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) )
19 7 18 nfald ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 ∀ 𝑦 ( ∃ 𝑤 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) )
20 nfcvd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑦 𝑤 )
21 nfcvf2 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 )
22 21 adantr ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑦 𝑥 )
23 20 22 nfeqd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑦 𝑤 = 𝑥 )
24 7 23 nfan1 ⊢ Ⅎ 𝑦 ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 )
25 elequ2 ⊢ ( 𝑤 = 𝑥 → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥 ) )
26 elequ1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧 ) )
27 25 26 anbi12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) ) )
28 27 a1i ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑤 = 𝑥 → ( ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) ) ) )
29 4 16 28 cbvexd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∃ 𝑤 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) ↔ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) ) )
30 29 adantr ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∃ 𝑤 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) ↔ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) ) )
31 25 adantl ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑥 ) )
32 30 31 imbi12d ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ( ∃ 𝑤 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) ↔ ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
33 24 32 albid ⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) ∧ 𝑤 = 𝑥 ) → ( ∀ 𝑦 ( ∃ 𝑤 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) ↔ ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
34 33 ex ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑤 = 𝑥 → ( ∀ 𝑦 ( ∃ 𝑤 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) ↔ ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) ) )
35 4 19 34 cbvexd ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑧 ) → 𝑦 ∈ 𝑤 ) ↔ ∃ 𝑥 ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
36 1 35 mpbii ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ∃ 𝑥 ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
37 36 ex ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) ) )
38 nfae ⊢ Ⅎ 𝑦 ∀ 𝑥 𝑥 = 𝑦
39 nfae ⊢ Ⅎ 𝑥 ∀ 𝑥 𝑥 = 𝑦
40 elirrv ⊢ ¬ 𝑦 ∈ 𝑦
41 elequ2 ⊢ ( 𝑥 = 𝑦 → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) )
42 40 41 mtbiri ⊢ ( 𝑥 = 𝑦 → ¬ 𝑦 ∈ 𝑥 )
43 42 intnanrd ⊢ ( 𝑥 = 𝑦 → ¬ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) )
44 43 sps ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ¬ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) )
45 39 44 nexd ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ¬ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) )
46 45 pm2.21d ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
47 38 46 alrimi ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
48 47 19.8ad ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
49 nfae ⊢ Ⅎ 𝑦 ∀ 𝑥 𝑥 = 𝑧
50 nfae ⊢ Ⅎ 𝑥 ∀ 𝑥 𝑥 = 𝑧
51 elirrv ⊢ ¬ 𝑧 ∈ 𝑧
52 elequ1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑧 ↔ 𝑧 ∈ 𝑧 ) )
53 51 52 mtbiri ⊢ ( 𝑥 = 𝑧 → ¬ 𝑥 ∈ 𝑧 )
54 53 intnand ⊢ ( 𝑥 = 𝑧 → ¬ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) )
55 54 sps ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ¬ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) )
56 50 55 nexd ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ¬ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) )
57 56 pm2.21d ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
58 49 57 alrimi ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
59 58 19.8ad ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 ) )
60 37 48 59 pm2.61ii ⊢ ∃ 𝑥 ∀ 𝑦 ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑥 )