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

Metamath Proof Explorer

Theorem iinexg

Description: The existence of a class intersection. x is normally a free-variable parameter in B , which should be read B ( x ) . (Contributed by FL, 19-Sep-2011)

Ref Expression
Assertion iinexg ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V )

Proof

Step Hyp Ref Expression
1 dfiin2g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
2 1 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
3 elisset ⊢ ( 𝐵 ∈ 𝐶 → ∃ 𝑦 𝑦 = 𝐵 )
4 3 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝐶 → ∃ 𝑦 𝑦 = 𝐵 )
5 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝐶 → ∃ 𝑦 𝑦 = 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝐶 → ∃ 𝑦 𝑦 = 𝐵 ) )
6 4 5 mpan2 ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝐶 → ∃ 𝑦 𝑦 = 𝐵 ) )
7 r19.35 ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐵 ∈ 𝐶 → ∃ 𝑦 𝑦 = 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ) )
8 6 7 sylib ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ) )
9 8 imp ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 )
10 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 = 𝐵 ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
11 9 10 sylib ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
12 abn0 ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 )
13 11 12 sylibr ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≠ ∅ )
14 intex ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ≠ ∅ ↔ ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ V )
15 13 14 sylib ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ∈ V )
16 2 15 eqeltrd ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ V )