Metamath Proof Explorer

Theorem ax6e2ndVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2nd is ax6e2ndVD without virtual deductions and was automatically derived from ax6e2ndVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

1:: |- E. y y = v
2:: |- u e.V
3:1,2: |- ( u e. V /\ E. y y = v )
4:3: |- E. y ( u e.V /\ y = v )
5:: |- ( u e. V <-> E. x x = u )
6:5: |- ( ( u e.V /\ y = v ) <-> ( E. x x = u /\ y = v ) )
7:6: |- ( E. y ( u e. V /\ y = v ) <-> E. y ( E. x x = u /\ y = v ) )
8:4,7: |- E. y ( E. x x = u /\ y = v )
9:: |- ( z = v -> A. x z = v )
10:: |- ( y = v -> A. z y = v )
11:: |- (. z = y ->. z = y ).
12:11: |- (. z = y ->. ( z = v <-> y = v ) ).
120:11: |- ( z = y -> ( z = v <-> y = v ) )
13:9,10,120: |- ( -. A. x x = y -> ( y = v -> A. x y = v ) )
14:: |- (. -. A. x x = y ->. -. A. x x = y ).
15:14,13: |- (. -. A. x x = y ->. ( y = v -> A. x y = v ) ).
16:15: |- ( -. A. x x = y -> ( y = v -> A. x y = v ) )
17:16: |- ( A. x -. A. x x = y -> A. x ( y = v -> A. x y = v ) )
18:: |- ( -. A. x x = y -> A. x -. A. x x = y )
19:17,18: |- ( -. A. x x = y -> A. x ( y = v -> A. x y = v ) )
20:14,19: |- (. -. A. x x = y ->. A. x ( y = v -> A. x y = v ) ).
21:20: |- (. -. A. x x = y ->. ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) ).
22:21: |- ( -. A. x x = y -> ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
23:22: |- ( A. y -. A. x x = y -> A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
24:: |- ( -. A. x x = y -> A. y -. A. x x = y )
25:23,24: |- ( -. A. x x = y -> A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
26:14,25: |- (. -. A. x x = y ->. A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) ).
27:26: |- (. -. A. x x = y ->. ( E. y ( E. x x = u /\ y = v ) -> E. y E. x ( x = u /\ y = v ) ) ).
28:8,27: |- (. -. A. x x = y ->. E. y E. x ( x = u /\ y = v ) ).
29:28: |- (. -. A. x x = y ->. E. x E. y ( x = u /\ y = v ) ).
qed:29: |- ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )

Ref Expression
Assertion ax6e2ndVD ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑢 ∈ V
2 ax6e ⊢ ∃ 𝑦 𝑦 = 𝑣
3 1 2 pm3.2i ⊢ ( 𝑢 ∈ V ∧ ∃ 𝑦 𝑦 = 𝑣 )
4 19.42v ⊢ ( ∃ 𝑦 ( 𝑢 ∈ V ∧ 𝑦 = 𝑣 ) ↔ ( 𝑢 ∈ V ∧ ∃ 𝑦 𝑦 = 𝑣 ) )
5 4 biimpri ⊢ ( ( 𝑢 ∈ V ∧ ∃ 𝑦 𝑦 = 𝑣 ) → ∃ 𝑦 ( 𝑢 ∈ V ∧ 𝑦 = 𝑣 ) )
6 3 5 e0a ⊢ ∃ 𝑦 ( 𝑢 ∈ V ∧ 𝑦 = 𝑣 )
7 isset ⊢ ( 𝑢 ∈ V ↔ ∃ 𝑥 𝑥 = 𝑢 )
8 7 anbi1i ⊢ ( ( 𝑢 ∈ V ∧ 𝑦 = 𝑣 ) ↔ ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
9 8 exbii ⊢ ( ∃ 𝑦 ( 𝑢 ∈ V ∧ 𝑦 = 𝑣 ) ↔ ∃ 𝑦 ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
10 6 9 mpbi ⊢ ∃ 𝑦 ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )
11 idn1 ⊢ (    ¬ ∀ 𝑥 𝑥 = 𝑦    ▶    ¬ ∀ 𝑥 𝑥 = 𝑦    )
12 hbnae ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 )
13 hbn1 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 )
14 ax-5 ⊢ ( 𝑧 = 𝑣 → ∀ 𝑥 𝑧 = 𝑣 )
15 ax-5 ⊢ ( 𝑦 = 𝑣 → ∀ 𝑧 𝑦 = 𝑣 )
16 idn1 ⊢ (    𝑧 = 𝑦    ▶    𝑧 = 𝑦    )
17 equequ1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 = 𝑣 ↔ 𝑦 = 𝑣 ) )
18 16 17 e1a ⊢ (    𝑧 = 𝑦    ▶    ( 𝑧 = 𝑣 ↔ 𝑦 = 𝑣 )    )
19 18 in1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 = 𝑣 ↔ 𝑦 = 𝑣 ) )
20 14 15 19 dvelimh ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 ) )
21 11 20 e1a ⊢ (    ¬ ∀ 𝑥 𝑥 = 𝑦    ▶    ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 )    )
22 21 in1 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 ) )
23 22 alimi ⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 ) )
24 13 23 syl ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 ) )
25 11 24 e1a ⊢ (    ¬ ∀ 𝑥 𝑥 = 𝑦    ▶    ∀ 𝑥 ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 )    )
26 19.41rg ⊢ ( ∀ 𝑥 ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 ) → ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
27 25 26 e1a ⊢ (    ¬ ∀ 𝑥 𝑥 = 𝑦    ▶    ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )    )
28 27 in1 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
29 28 alimi ⊢ ( ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
30 12 29 syl ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
31 11 30 e1a ⊢ (    ¬ ∀ 𝑥 𝑥 = 𝑦    ▶    ∀ 𝑦 ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )    )
32 exim ⊢ ( ∀ 𝑦 ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) → ( ∃ 𝑦 ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
33 31 32 e1a ⊢ (    ¬ ∀ 𝑥 𝑥 = 𝑦    ▶    ( ∃ 𝑦 ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )    )
34 pm2.27 ⊢ ( ∃ 𝑦 ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ( ∃ 𝑦 ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
35 10 33 34 e01 ⊢ (    ¬ ∀ 𝑥 𝑥 = 𝑦    ▶    ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )    )
36 excomim ⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
37 35 36 e1a ⊢ (    ¬ ∀ 𝑥 𝑥 = 𝑦    ▶    ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )    )
38 37 in1 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )