Metamath Proof Explorer

Theorem elmapintrab

Description: Two ways to say a set is an element of the intersection of a class of images. (Contributed by RP, 16-Aug-2020)

Ref Expression
Hypotheses elmapintrab.ex ⊢ 𝐶 ∈ V
elmapintrab.sub ⊢ 𝐶 ⊆ 𝐵
Assertion elmapintrab ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ { 𝑤 ∈ 𝒫 𝐵 ∣ ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) } ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 elmapintrab.ex ⊢ 𝐶 ∈ V
2 elmapintrab.sub ⊢ 𝐶 ⊆ 𝐵
3 elintrabg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ { 𝑤 ∈ 𝒫 𝐵 ∣ ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) } ↔ ∀ 𝑤 ∈ 𝒫 𝐵 ( ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) )
4 df-ral ⊢ ( ∀ 𝑤 ∈ 𝒫 𝐵 ( ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝒫 𝐵 → ( ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) )
5 3 4 bitrdi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ { 𝑤 ∈ 𝒫 𝐵 ∣ ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) } ↔ ∀ 𝑤 ( 𝑤 ∈ 𝒫 𝐵 → ( ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) ) )
6 velpw ⊢ ( 𝑤 ∈ 𝒫 𝐵 ↔ 𝑤 ⊆ 𝐵 )
7 19.23v ⊢ ( ∀ 𝑥 ( ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ↔ ( ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) )
8 7 bicomi ⊢ ( ( ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ↔ ∀ 𝑥 ( ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) )
9 6 8 imbi12i ⊢ ( ( 𝑤 ∈ 𝒫 𝐵 → ( ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) ↔ ( 𝑤 ⊆ 𝐵 → ∀ 𝑥 ( ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) )
10 19.21v ⊢ ( ∀ 𝑥 ( 𝑤 ⊆ 𝐵 → ( ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) ↔ ( 𝑤 ⊆ 𝐵 → ∀ 𝑥 ( ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) )
11 bi2.04 ⊢ ( ( 𝑤 ⊆ 𝐵 → ( ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) ↔ ( ( 𝑤 = 𝐶 ∧ 𝜑 ) → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) )
12 impexp ⊢ ( ( ( 𝑤 = 𝐶 ∧ 𝜑 ) → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ↔ ( 𝑤 = 𝐶 → ( 𝜑 → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ) )
13 11 12 bitri ⊢ ( ( 𝑤 ⊆ 𝐵 → ( ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) ↔ ( 𝑤 = 𝐶 → ( 𝜑 → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ) )
14 13 albii ⊢ ( ∀ 𝑥 ( 𝑤 ⊆ 𝐵 → ( ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) ↔ ∀ 𝑥 ( 𝑤 = 𝐶 → ( 𝜑 → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ) )
15 9 10 14 3bitr2i ⊢ ( ( 𝑤 ∈ 𝒫 𝐵 → ( ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) ↔ ∀ 𝑥 ( 𝑤 = 𝐶 → ( 𝜑 → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ) )
16 15 albii ⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝒫 𝐵 → ( ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) ↔ ∀ 𝑤 ∀ 𝑥 ( 𝑤 = 𝐶 → ( 𝜑 → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ) )
17 alcom ⊢ ( ∀ 𝑤 ∀ 𝑥 ( 𝑤 = 𝐶 → ( 𝜑 → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ) ↔ ∀ 𝑥 ∀ 𝑤 ( 𝑤 = 𝐶 → ( 𝜑 → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ) )
18 sseq1 ⊢ ( 𝑤 = 𝐶 → ( 𝑤 ⊆ 𝐵 ↔ 𝐶 ⊆ 𝐵 ) )
19 eleq2 ⊢ ( 𝑤 = 𝐶 → ( 𝐴 ∈ 𝑤 ↔ 𝐴 ∈ 𝐶 ) )
20 2 sseli ⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ∈ 𝐵 )
21 20 pm4.71ri ⊢ ( 𝐴 ∈ 𝐶 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) )
22 19 21 bitrdi ⊢ ( 𝑤 = 𝐶 → ( 𝐴 ∈ 𝑤 ↔ ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) )
23 18 22 imbi12d ⊢ ( 𝑤 = 𝐶 → ( ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ↔ ( 𝐶 ⊆ 𝐵 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) ) )
24 23 imbi2d ⊢ ( 𝑤 = 𝐶 → ( ( 𝜑 → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ↔ ( 𝜑 → ( 𝐶 ⊆ 𝐵 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) ) ) )
25 1 24 ceqsalv ⊢ ( ∀ 𝑤 ( 𝑤 = 𝐶 → ( 𝜑 → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ) ↔ ( 𝜑 → ( 𝐶 ⊆ 𝐵 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) ) )
26 bi2.04 ⊢ ( ( 𝜑 → ( 𝐶 ⊆ 𝐵 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) ) ↔ ( 𝐶 ⊆ 𝐵 → ( 𝜑 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) ) )
27 pm5.5 ⊢ ( 𝐶 ⊆ 𝐵 → ( ( 𝐶 ⊆ 𝐵 → ( 𝜑 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) ) ↔ ( 𝜑 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) ) )
28 2 27 ax-mp ⊢ ( ( 𝐶 ⊆ 𝐵 → ( 𝜑 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) ) ↔ ( 𝜑 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) )
29 jcab ⊢ ( ( 𝜑 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) ↔ ( ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ( 𝜑 → 𝐴 ∈ 𝐶 ) ) )
30 28 29 bitri ⊢ ( ( 𝐶 ⊆ 𝐵 → ( 𝜑 → ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) ) ) ↔ ( ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ( 𝜑 → 𝐴 ∈ 𝐶 ) ) )
31 25 26 30 3bitri ⊢ ( ∀ 𝑤 ( 𝑤 = 𝐶 → ( 𝜑 → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ) ↔ ( ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ( 𝜑 → 𝐴 ∈ 𝐶 ) ) )
32 31 albii ⊢ ( ∀ 𝑥 ∀ 𝑤 ( 𝑤 = 𝐶 → ( 𝜑 → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ) ↔ ∀ 𝑥 ( ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ( 𝜑 → 𝐴 ∈ 𝐶 ) ) )
33 19.26 ⊢ ( ∀ 𝑥 ( ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ( 𝜑 → 𝐴 ∈ 𝐶 ) ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐶 ) ) )
34 19.23v ⊢ ( ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐵 ) ↔ ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) )
35 34 anbi1i ⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐶 ) ) ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐶 ) ) )
36 32 33 35 3bitri ⊢ ( ∀ 𝑥 ∀ 𝑤 ( 𝑤 = 𝐶 → ( 𝜑 → ( 𝑤 ⊆ 𝐵 → 𝐴 ∈ 𝑤 ) ) ) ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐶 ) ) )
37 16 17 36 3bitri ⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝒫 𝐵 → ( ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) → 𝐴 ∈ 𝑤 ) ) ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐶 ) ) )
38 5 37 bitrdi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ { 𝑤 ∈ 𝒫 𝐵 ∣ ∃ 𝑥 ( 𝑤 = 𝐶 ∧ 𝜑 ) } ↔ ( ( ∃ 𝑥 𝜑 → 𝐴 ∈ 𝐵 ) ∧ ∀ 𝑥 ( 𝜑 → 𝐴 ∈ 𝐶 ) ) ) )