Metamath Proof Explorer

Theorem ax6e2ndeq

Description: "At least two sets exist" expressed in the form of dtru is logically equivalent to the same expressed in a form similar to ax6e if dtru is false implies u = v . ax6e2ndeq is derived from ax6e2ndeqVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6e2ndeq ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )

Proof

Step Hyp Ref Expression
1 ax6e2nd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
2 ax6e2eq ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
3 1 a1d ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ) )
4 2 3 pm2.61i ⊢ ( 𝑢 = 𝑣 → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
5 1 4 jaoi ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
6 olc ⊢ ( 𝑢 = 𝑣 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) )
7 6 a1d ⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ) )
8 excom ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
9 neeq1 ⊢ ( 𝑥 = 𝑢 → ( 𝑥 ≠ 𝑣 ↔ 𝑢 ≠ 𝑣 ) )
10 9 biimprcd ⊢ ( 𝑢 ≠ 𝑣 → ( 𝑥 = 𝑢 → 𝑥 ≠ 𝑣 ) )
11 10 adantrd ⊢ ( 𝑢 ≠ 𝑣 → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑥 ≠ 𝑣 ) )
12 simpr ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑦 = 𝑣 )
13 12 a1i ⊢ ( 𝑢 ≠ 𝑣 → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑦 = 𝑣 ) )
14 neeq2 ⊢ ( 𝑦 = 𝑣 → ( 𝑥 ≠ 𝑦 ↔ 𝑥 ≠ 𝑣 ) )
15 14 biimprcd ⊢ ( 𝑥 ≠ 𝑣 → ( 𝑦 = 𝑣 → 𝑥 ≠ 𝑦 ) )
16 11 13 15 syl6c ⊢ ( 𝑢 ≠ 𝑣 → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑥 ≠ 𝑦 ) )
17 sp ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 )
18 17 necon3ai ⊢ ( 𝑥 ≠ 𝑦 → ¬ ∀ 𝑥 𝑥 = 𝑦 )
19 16 18 syl6 ⊢ ( 𝑢 ≠ 𝑣 → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
20 19 eximdv ⊢ ( 𝑢 ≠ 𝑣 → ( ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
21 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
22 21 19.9 ⊢ ( ∃ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 )
23 20 22 syl6ib ⊢ ( 𝑢 ≠ 𝑣 → ( ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
24 23 eximdv ⊢ ( 𝑢 ≠ 𝑣 → ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
25 8 24 syl5bi ⊢ ( 𝑢 ≠ 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
26 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
27 26 19.9 ⊢ ( ∃ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 )
28 25 27 syl6ib ⊢ ( 𝑢 ≠ 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ¬ ∀ 𝑥 𝑥 = 𝑦 ) )
29 orc ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) )
30 28 29 syl6 ⊢ ( 𝑢 ≠ 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ) )
31 7 30 pm2.61ine ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) )
32 5 31 impbii ⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )