Metamath Proof Explorer

Theorem epfrs

Description: The strong form of the Axiom of Regularity (no sethood requirement on A ), with the axiom itself present as an antecedent. See also zfregs . (Contributed by Mario Carneiro, 22-Mar-2013)

Ref Expression
Assertion epfrs ( ( E Fr 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐴 )
2 snssi ⊢ ( 𝑧 ∈ 𝐴 → { 𝑧 } ⊆ 𝐴 )
3 2 anim2i ⊢ ( ( { 𝑧 } ⊆ 𝑦 ∧ 𝑧 ∈ 𝐴 ) → ( { 𝑧 } ⊆ 𝑦 ∧ { 𝑧 } ⊆ 𝐴 ) )
4 ssin ⊢ ( ( { 𝑧 } ⊆ 𝑦 ∧ { 𝑧 } ⊆ 𝐴 ) ↔ { 𝑧 } ⊆ ( 𝑦 ∩ 𝐴 ) )
5 vex ⊢ 𝑧 ∈ V
6 5 snss ⊢ ( 𝑧 ∈ ( 𝑦 ∩ 𝐴 ) ↔ { 𝑧 } ⊆ ( 𝑦 ∩ 𝐴 ) )
7 4 6 bitr4i ⊢ ( ( { 𝑧 } ⊆ 𝑦 ∧ { 𝑧 } ⊆ 𝐴 ) ↔ 𝑧 ∈ ( 𝑦 ∩ 𝐴 ) )
8 3 7 sylib ⊢ ( ( { 𝑧 } ⊆ 𝑦 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ( 𝑦 ∩ 𝐴 ) )
9 8 ne0d ⊢ ( ( { 𝑧 } ⊆ 𝑦 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 ∩ 𝐴 ) ≠ ∅ )
10 inss2 ⊢ ( 𝑦 ∩ 𝐴 ) ⊆ 𝐴
11 vex ⊢ 𝑦 ∈ V
12 11 inex1 ⊢ ( 𝑦 ∩ 𝐴 ) ∈ V
13 12 epfrc ⊢ ( ( E Fr 𝐴 ∧ ( 𝑦 ∩ 𝐴 ) ⊆ 𝐴 ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ) → ∃ 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ )
14 10 13 mp3an2 ⊢ ( ( E Fr 𝐴 ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ) → ∃ 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ )
15 elin ⊢ ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ↔ ( 𝑥 ∈ 𝑦 ∧ 𝑥 ∈ 𝐴 ) )
16 15 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ ) ↔ ( ( 𝑥 ∈ 𝑦 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ ) )
17 anass ⊢ ( ( ( 𝑥 ∈ 𝑦 ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ ) ) )
18 16 17 bitri ⊢ ( ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ ) ) )
19 n0 ⊢ ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) )
20 elinel1 ⊢ ( 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) → 𝑤 ∈ 𝑥 )
21 20 ancri ⊢ ( 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) → ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) ) )
22 trel ⊢ ( Tr 𝑦 → ( ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) → 𝑤 ∈ 𝑦 ) )
23 inass ⊢ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ( 𝑦 ∩ ( 𝐴 ∩ 𝑥 ) )
24 incom ⊢ ( 𝐴 ∩ 𝑥 ) = ( 𝑥 ∩ 𝐴 )
25 24 ineq2i ⊢ ( 𝑦 ∩ ( 𝐴 ∩ 𝑥 ) ) = ( 𝑦 ∩ ( 𝑥 ∩ 𝐴 ) )
26 23 25 eqtri ⊢ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ( 𝑦 ∩ ( 𝑥 ∩ 𝐴 ) )
27 26 eleq2i ⊢ ( 𝑤 ∈ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ↔ 𝑤 ∈ ( 𝑦 ∩ ( 𝑥 ∩ 𝐴 ) ) )
28 elin ⊢ ( 𝑤 ∈ ( 𝑦 ∩ ( 𝑥 ∩ 𝐴 ) ) ↔ ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) ) )
29 27 28 bitr2i ⊢ ( ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) ) ↔ 𝑤 ∈ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) )
30 ne0i ⊢ ( 𝑤 ∈ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) → ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ≠ ∅ )
31 29 30 sylbi ⊢ ( ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) ) → ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ≠ ∅ )
32 31 ex ⊢ ( 𝑤 ∈ 𝑦 → ( 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) → ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ≠ ∅ ) )
33 22 32 syl6 ⊢ ( Tr 𝑦 → ( ( 𝑤 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) → ( 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) → ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ≠ ∅ ) ) )
34 33 expd ⊢ ( Tr 𝑦 → ( 𝑤 ∈ 𝑥 → ( 𝑥 ∈ 𝑦 → ( 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) → ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ≠ ∅ ) ) ) )
35 34 com34 ⊢ ( Tr 𝑦 → ( 𝑤 ∈ 𝑥 → ( 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ≠ ∅ ) ) ) )
36 35 impd ⊢ ( Tr 𝑦 → ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) ) → ( 𝑥 ∈ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ≠ ∅ ) ) )
37 21 36 syl5 ⊢ ( Tr 𝑦 → ( 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ≠ ∅ ) ) )
38 37 exlimdv ⊢ ( Tr 𝑦 → ( ∃ 𝑤 𝑤 ∈ ( 𝑥 ∩ 𝐴 ) → ( 𝑥 ∈ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ≠ ∅ ) ) )
39 19 38 syl5bi ⊢ ( Tr 𝑦 → ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ → ( 𝑥 ∈ 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ≠ ∅ ) ) )
40 39 com23 ⊢ ( Tr 𝑦 → ( 𝑥 ∈ 𝑦 → ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ → ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ≠ ∅ ) ) )
41 40 imp ⊢ ( ( Tr 𝑦 ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝑥 ∩ 𝐴 ) ≠ ∅ → ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) ≠ ∅ ) )
42 41 necon4d ⊢ ( ( Tr 𝑦 ∧ 𝑥 ∈ 𝑦 ) → ( ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ → ( 𝑥 ∩ 𝐴 ) = ∅ ) )
43 42 anim2d ⊢ ( ( Tr 𝑦 ∧ 𝑥 ∈ 𝑦 ) → ( ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ ) → ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∩ 𝐴 ) = ∅ ) ) )
44 43 expimpd ⊢ ( Tr 𝑦 → ( ( 𝑥 ∈ 𝑦 ∧ ( 𝑥 ∈ 𝐴 ∧ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ ) ) → ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∩ 𝐴 ) = ∅ ) ) )
45 18 44 syl5bi ⊢ ( Tr 𝑦 → ( ( 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ∧ ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ ) → ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∩ 𝐴 ) = ∅ ) ) )
46 45 reximdv2 ⊢ ( Tr 𝑦 → ( ∃ 𝑥 ∈ ( 𝑦 ∩ 𝐴 ) ( ( 𝑦 ∩ 𝐴 ) ∩ 𝑥 ) = ∅ → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) )
47 14 46 syl5 ⊢ ( Tr 𝑦 → ( ( E Fr 𝐴 ∧ ( 𝑦 ∩ 𝐴 ) ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) )
48 47 expcomd ⊢ ( Tr 𝑦 → ( ( 𝑦 ∩ 𝐴 ) ≠ ∅ → ( E Fr 𝐴 → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) ) )
49 9 48 syl5 ⊢ ( Tr 𝑦 → ( ( { 𝑧 } ⊆ 𝑦 ∧ 𝑧 ∈ 𝐴 ) → ( E Fr 𝐴 → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) ) )
50 49 expd ⊢ ( Tr 𝑦 → ( { 𝑧 } ⊆ 𝑦 → ( 𝑧 ∈ 𝐴 → ( E Fr 𝐴 → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) ) ) )
51 50 impcom ⊢ ( ( { 𝑧 } ⊆ 𝑦 ∧ Tr 𝑦 ) → ( 𝑧 ∈ 𝐴 → ( E Fr 𝐴 → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) ) )
52 51 3adant3 ⊢ ( ( { 𝑧 } ⊆ 𝑦 ∧ Tr 𝑦 ∧ ∀ 𝑤 ( ( { 𝑧 } ⊆ 𝑤 ∧ Tr 𝑤 ) → 𝑦 ⊆ 𝑤 ) ) → ( 𝑧 ∈ 𝐴 → ( E Fr 𝐴 → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) ) )
53 snex ⊢ { 𝑧 } ∈ V
54 53 tz9.1 ⊢ ∃ 𝑦 ( { 𝑧 } ⊆ 𝑦 ∧ Tr 𝑦 ∧ ∀ 𝑤 ( ( { 𝑧 } ⊆ 𝑤 ∧ Tr 𝑤 ) → 𝑦 ⊆ 𝑤 ) )
55 52 54 exlimiiv ⊢ ( 𝑧 ∈ 𝐴 → ( E Fr 𝐴 → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) )
56 55 exlimiv ⊢ ( ∃ 𝑧 𝑧 ∈ 𝐴 → ( E Fr 𝐴 → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) )
57 1 56 sylbi ⊢ ( 𝐴 ≠ ∅ → ( E Fr 𝐴 → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ ) )
58 57 impcom ⊢ ( ( E Fr 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ )