Metamath Proof Explorer

Theorem dfiin2g

Description: Alternate definition of indexed intersection when B is a set. (Contributed by Jeff Hankins, 27-Aug-2009)

Ref Expression
Assertion dfiin2g ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )

Proof

Step Hyp Ref Expression
1 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) )
2 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) )
3 eleq2 ⊢ ( 𝑧 = 𝐵 → ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝐵 ) )
4 3 biimprcd ⊢ ( 𝑤 ∈ 𝐵 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) )
5 4 alrimiv ⊢ ( 𝑤 ∈ 𝐵 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) )
6 eqid ⊢ 𝐵 = 𝐵
7 eqeq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 = 𝐵 ↔ 𝐵 = 𝐵 ) )
8 7 3 imbi12d ⊢ ( 𝑧 = 𝐵 → ( ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ( 𝐵 = 𝐵 → 𝑤 ∈ 𝐵 ) ) )
9 8 spcgv ⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) → ( 𝐵 = 𝐵 → 𝑤 ∈ 𝐵 ) ) )
10 6 9 mpii ⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) → 𝑤 ∈ 𝐵 ) )
11 5 10 impbid2 ⊢ ( 𝐵 ∈ 𝐶 → ( 𝑤 ∈ 𝐵 ↔ ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
12 11 imim2i ⊢ ( ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 → ( 𝑤 ∈ 𝐵 ↔ ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
13 12 pm5.74d ⊢ ( ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
14 13 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
15 albi ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
16 14 15 syl ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
17 2 16 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
18 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
19 18 albii ⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
20 alcom ⊢ ( ∀ 𝑥 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ↔ ∀ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
21 19 20 bitr4i ⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
22 r19.23v ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) )
23 vex ⊢ 𝑧 ∈ V
24 eqeq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 = 𝐵 ↔ 𝑧 = 𝐵 ) )
25 24 rexbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
26 23 25 elab ⊢ ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
27 26 imbi1i ⊢ ( ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) )
28 22 27 bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) )
29 28 albii ⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) )
30 19.21v ⊢ ( ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
31 30 albii ⊢ ( ∀ 𝑥 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
32 21 29 31 3bitr3ri ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) )
33 17 32 bitrdi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) ) )
34 1 33 bitrid ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) ) )
35 34 abbidv ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → { 𝑤 ∣ ∀ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 } = { 𝑤 ∣ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) } )
36 df-iin ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = { 𝑤 ∣ ∀ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 }
37 df-int ⊢ ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } = { 𝑤 ∣ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) }
38 35 36 37 3eqtr4g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )