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

Metamath Proof Explorer

Theorem intab

Description: The intersection of a special case of a class abstraction. y may be free in ph and A , which can be thought of a ph ( y ) and A ( y ) . Typically, abrexex2 or abexssex can be used to satisfy the second hypothesis. (Contributed by NM, 28-Jul-2006) (Proof shortened by Mario Carneiro, 14-Nov-2016)

Ref Expression
Hypotheses intab.1 ⊢ 𝐴 ∈ V
intab.2 ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) } ∈ V
Assertion intab ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) }

Proof

Step Hyp Ref Expression
1 intab.1 ⊢ 𝐴 ∈ V
2 intab.2 ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) } ∈ V
3 eqeq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 = 𝐴 ↔ 𝑥 = 𝐴 ) )
4 3 anbi2d ⊢ ( 𝑧 = 𝑥 → ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ↔ ( 𝜑 ∧ 𝑥 = 𝐴 ) ) )
5 4 exbidv ⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ↔ ∃ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) ) )
6 5 cbvabv ⊢ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) }
7 6 2 eqeltri ⊢ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ∈ V
8 nfe1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 )
9 8 nfab ⊢ Ⅎ 𝑦 { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) }
10 9 nfeq2 ⊢ Ⅎ 𝑦 𝑥 = { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) }
11 eleq2 ⊢ ( 𝑥 = { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ) )
12 11 imbi2d ⊢ ( 𝑥 = { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } → ( ( 𝜑 → 𝐴 ∈ 𝑥 ) ↔ ( 𝜑 → 𝐴 ∈ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ) ) )
13 10 12 albid ⊢ ( 𝑥 = { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } → ( ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) ↔ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ) ) )
14 7 13 elab ⊢ ( { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ∈ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } ↔ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ) )
15 19.8a ⊢ ( ( 𝜑 ∧ 𝑧 = 𝐴 ) → ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) )
16 15 ex ⊢ ( 𝜑 → ( 𝑧 = 𝐴 → ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ) )
17 16 alrimiv ⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 = 𝐴 → ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ) )
18 1 sbc6 ⊢ ( [ 𝐴 / 𝑧 ] ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ↔ ∀ 𝑧 ( 𝑧 = 𝐴 → ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ) )
19 17 18 sylibr ⊢ ( 𝜑 → [ 𝐴 / 𝑧 ] ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) )
20 df-sbc ⊢ ( [ 𝐴 / 𝑧 ] ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ↔ 𝐴 ∈ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } )
21 19 20 sylib ⊢ ( 𝜑 → 𝐴 ∈ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } )
22 14 21 mpgbir ⊢ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ∈ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) }
23 intss1 ⊢ ( { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ∈ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } → ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } ⊆ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } )
24 22 23 ax-mp ⊢ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } ⊆ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) }
25 19.29r ⊢ ( ( ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → ∃ 𝑦 ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) )
26 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → 𝑧 = 𝐴 )
27 pm3.35 ⊢ ( ( 𝜑 ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → 𝐴 ∈ 𝑥 )
28 27 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → 𝐴 ∈ 𝑥 )
29 26 28 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → 𝑧 ∈ 𝑥 )
30 29 exlimiv ⊢ ( ∃ 𝑦 ( ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → 𝑧 ∈ 𝑥 )
31 25 30 syl ⊢ ( ( ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) ∧ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) ) → 𝑧 ∈ 𝑥 )
32 31 ex ⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) → ( ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
33 32 alrimiv ⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) → ∀ 𝑥 ( ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
34 vex ⊢ 𝑧 ∈ V
35 34 elintab ⊢ ( 𝑧 ∈ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } ↔ ∀ 𝑥 ( ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
36 33 35 sylibr ⊢ ( ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) → 𝑧 ∈ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } )
37 36 abssi ⊢ { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) } ⊆ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) }
38 24 37 eqssi ⊢ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑧 = 𝐴 ) }
39 38 6 eqtri ⊢ ∩ { 𝑥 ∣ ∀ 𝑦 ( 𝜑 → 𝐴 ∈ 𝑥 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) }