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

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 clel4g ⊢ ( 𝐵 ∈ 𝐶 → ( 𝑤 ∈ 𝐵 ↔ ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
4 3 imim2i ⊢ ( ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 → ( 𝑤 ∈ 𝐵 ↔ ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
5 4 pm5.74d ⊢ ( ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
6 5 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
7 albi ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
8 6 7 syl ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝐶 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
9 2 8 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ) )
10 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
11 10 albii ⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
12 alcom ⊢ ( ∀ 𝑥 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ↔ ∀ 𝑧 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
13 11 12 bitr4i ⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
14 r19.23v ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) )
15 vex ⊢ 𝑧 ∈ V
16 eqeq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 = 𝐵 ↔ 𝑧 = 𝐵 ) )
17 16 rexbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
18 15 17 elab ⊢ ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
19 18 imbi1i ⊢ ( ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) ↔ ( ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) )
20 14 19 bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) )
21 20 albii ⊢ ( ∀ 𝑧 ∀ 𝑥 ∈ 𝐴 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) )
22 19.21v ⊢ ( ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
23 22 albii ⊢ ( ∀ 𝑥 ∀ 𝑧 ( 𝑥 ∈ 𝐴 → ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) )
24 13 21 23 3bitr3ri ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑧 ( 𝑧 = 𝐵 → 𝑤 ∈ 𝑧 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) )
25 9 24 bitrdi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑤 ∈ 𝐵 ) ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) ) )
26 1 25 bitrid ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) ) )
27 26 abbidv ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → { 𝑤 ∣ ∀ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 } = { 𝑤 ∣ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) } )
28 df-iin ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = { 𝑤 ∣ ∀ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 }
29 df-int ⊢ ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } = { 𝑤 ∣ ∀ 𝑧 ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } → 𝑤 ∈ 𝑧 ) }
30 27 28 29 3eqtr4g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )