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	⊢ ( 𝐴 ≠ ∅ → ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )