Theorem zfregs2VD

Description: Virtual deduction proof of zfregs2 . (Contributed by Alan Sare, 24-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		idn1	⊢ (    𝐴 ≠ ∅    ▶    𝐴 ≠ ∅    )
2		zfregs	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ )
3	1 2	e1a	⊢ (    𝐴 ≠ ∅    ▶    ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅    )
4		incom	⊢ ( 𝑥 ∩ 𝐴 ) = ( 𝐴 ∩ 𝑥 )
5	4	eqeq1i	⊢ ( ( 𝑥 ∩ 𝐴 ) = ∅ ↔ ( 𝐴 ∩ 𝑥 ) = ∅ )
6	5	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∩ 𝑥 ) = ∅ )
7	3 6	e1bi	⊢ (    𝐴 ≠ ∅    ▶    ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∩ 𝑥 ) = ∅    )
8		disj1	⊢ ( ( 𝐴 ∩ 𝑥 ) = ∅ ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝑥 ) )
9	8	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∩ 𝑥 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝑥 ) )
10	7 9	e1bi	⊢ (    𝐴 ≠ ∅    ▶    ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝑥 )    )
11		alinexa	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝑥 ) ↔ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
12	11	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝑦 ∈ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
13	10 12	e1bi	⊢ (    𝐴 ≠ ∅    ▶    ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 )    )
14		dfrex2	⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ¬ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
15	13 14	e1bi	⊢ (    𝐴 ≠ ∅    ▶    ¬ ∀ 𝑥 ∈ 𝐴 ¬ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 )    )
16		notnotr	⊢ ( ¬ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
17		notnot	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) → ¬ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
18	16 17	impbii	⊢ ( ¬ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
19	18	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
20	19	notbii	⊢ ( ¬ ∀ 𝑥 ∈ 𝐴 ¬ ¬ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )
21	15 20	e1bi	⊢ (    𝐴 ≠ ∅    ▶    ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 )    )
22	21	in1	⊢ ( 𝐴 ≠ ∅ → ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) )