Metamath Proof Explorer

Theorem ax6e2ndALT

Description: If at least two sets exist ( dtru ), then the same is true expressed in an alternate form similar to the form of ax6e . The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndVD . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

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

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 ax-mp ⊢ ∃ 𝑦 ( 𝑢 ∈ V ∧ 𝑦 = 𝑣 )
7 isset ⊢ ( 𝑢 ∈ V ↔ ∃ 𝑥 𝑥 = 𝑢 )
8 7 anbi1i ⊢ ( ( 𝑢 ∈ V ∧ 𝑦 = 𝑣 ) ↔ ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
9 8 exbii ⊢ ( ∃ 𝑦 ( 𝑢 ∈ V ∧ 𝑦 = 𝑣 ) ↔ ∃ 𝑦 ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
10 6 9 mpbi ⊢ ∃ 𝑦 ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )
11 id ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ¬ ∀ 𝑥 𝑥 = 𝑦 )
12 hbnae ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 )
13 hbn1 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 )
14 ax-5 ⊢ ( 𝑧 = 𝑣 → ∀ 𝑥 𝑧 = 𝑣 )
15 ax-5 ⊢ ( 𝑦 = 𝑣 → ∀ 𝑧 𝑦 = 𝑣 )
16 id ⊢ ( 𝑧 = 𝑦 → 𝑧 = 𝑦 )
17 equequ1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 = 𝑣 ↔ 𝑦 = 𝑣 ) )
18 17 a1i ⊢ ( ( 𝑧 = 𝑦 → 𝑧 = 𝑦 ) → ( 𝑧 = 𝑦 → ( 𝑧 = 𝑣 ↔ 𝑦 = 𝑣 ) ) )
19 16 18 ax-mp ⊢ ( 𝑧 = 𝑦 → ( 𝑧 = 𝑣 ↔ 𝑦 = 𝑣 ) )
20 14 15 19 dvelimh ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 ) )
21 11 20 syl ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 ) )
22 21 idiALT ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 ) )
23 22 alimi ⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 ) )
24 13 23 syl ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 ) )
25 11 24 syl ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 ) )
26 19.41rg ⊢ ( ∀ 𝑥 ( 𝑦 = 𝑣 → ∀ 𝑥 𝑦 = 𝑣 ) → ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
27 25 26 syl ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
28 27 idiALT ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
29 28 alimi ⊢ ( ∀ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
30 12 29 syl ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
31 11 30 syl ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
32 exim ⊢ ( ∀ 𝑦 ( ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) → ( ∃ 𝑦 ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
33 31 32 syl ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑦 ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
34 pm3.35 ⊢ ( ( ∃ 𝑦 ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( ∃ 𝑦 ( ∃ 𝑥 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
35 10 33 34 sylancr ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
36 excomim ⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
37 35 36 syl ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
38 37 idiALT ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )