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

Metamath Proof Explorer

Theorem zfregs2

Description: Alternate strong form of the Axiom of Regularity. Not every element of a nonempty class contains some element of that class. (Contributed by Alan Sare, 24-Oct-2011) (Proof shortened by Wolf Lammen, 27-Sep-2013)

Ref Expression
Assertion zfregs2 ( 𝐴 ≠ ∅ → ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 zfregs ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ )
2 incom ⊢ ( 𝑥 ∩ 𝐴 ) = ( 𝐴 ∩ 𝑥 )
3 2 eqeq1i ⊢ ( ( 𝑥 ∩ 𝐴 ) = ∅ ↔ ( 𝐴 ∩ 𝑥 ) = ∅ )
4 3 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∩ 𝑥 ) = ∅ )
5 1 4 sylib ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∩ 𝑥 ) = ∅ )
6 disj1 ⊢ ( ( 𝐴 ∩ 𝑥 ) = ∅ ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝑥 ) )
7 6 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∩ 𝑥 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝑥 ) )
8 5 7 sylib ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝑥 ) )
9 alinexa ⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝑥 ) ↔ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
10 9 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
11 8 10 sylib ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
12 dfrex2 ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
13 11 12 sylib ⊢ ( 𝐴 ≠ ∅ → ¬ ∀ 𝑥 ∈ 𝐴 ¬ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
14 notnotb ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ↔ ¬ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
15 14 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ¬ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
16 13 15 sylnibr ⊢ ( 𝐴 ≠ ∅ → ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )