Metamath Proof Explorer

Theorem elintima

Description: Element of intersection of images. (Contributed by RP, 13-Apr-2020)

Ref Expression
Assertion elintima ( 𝑦 ∈ ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑦 ∈ V
2 1 elint2 ⊢ ( 𝑦 ∈ ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } ↔ ∀ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } 𝑦 ∈ 𝑧 )
3 elequ2 ⊢ ( 𝑧 = 𝑥 → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑥 ) )
4 3 ralab2 ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } 𝑦 ∈ 𝑧 ↔ ∀ 𝑥 ( ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) → 𝑦 ∈ 𝑥 ) )
5 df-rex ⊢ ( ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) ↔ ∃ 𝑎 ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) )
6 5 imbi1i ⊢ ( ( ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) → 𝑦 ∈ 𝑥 ) ↔ ( ∃ 𝑎 ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → 𝑦 ∈ 𝑥 ) )
7 19.23v ⊢ ( ∀ 𝑎 ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → 𝑦 ∈ 𝑥 ) ↔ ( ∃ 𝑎 ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → 𝑦 ∈ 𝑥 ) )
8 simpr ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → 𝑥 = ( 𝑎 “ 𝐵 ) )
9 8 eleq2d ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ ( 𝑎 “ 𝐵 ) ) )
10 9 pm5.74i ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → 𝑦 ∈ 𝑥 ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → 𝑦 ∈ ( 𝑎 “ 𝐵 ) ) )
11 1 elima ⊢ ( 𝑦 ∈ ( 𝑎 “ 𝐵 ) ↔ ∃ 𝑏 ∈ 𝐵 𝑏 𝑎 𝑦 )
12 df-br ⊢ ( 𝑏 𝑎 𝑦 ↔ ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
13 12 rexbii ⊢ ( ∃ 𝑏 ∈ 𝐵 𝑏 𝑎 𝑦 ↔ ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
14 11 13 bitri ⊢ ( 𝑦 ∈ ( 𝑎 “ 𝐵 ) ↔ ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
15 14 imbi2i ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → 𝑦 ∈ ( 𝑎 “ 𝐵 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
16 10 15 bitri ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → 𝑦 ∈ 𝑥 ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
17 16 albii ⊢ ( ∀ 𝑎 ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑎 ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
18 6 7 17 3bitr2i ⊢ ( ( ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑎 ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
19 18 albii ⊢ ( ∀ 𝑥 ( ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑎 ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
20 19.23v ⊢ ( ∀ 𝑥 ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) ↔ ( ∃ 𝑥 ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
21 vex ⊢ 𝑎 ∈ V
22 21 imaex ⊢ ( 𝑎 “ 𝐵 ) ∈ V
23 22 isseti ⊢ ∃ 𝑥 𝑥 = ( 𝑎 “ 𝐵 )
24 19.42v ⊢ ( ∃ 𝑥 ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) ↔ ( 𝑎 ∈ 𝐴 ∧ ∃ 𝑥 𝑥 = ( 𝑎 “ 𝐵 ) ) )
25 23 24 mpbiran2 ⊢ ( ∃ 𝑥 ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) ↔ 𝑎 ∈ 𝐴 )
26 25 imbi1i ⊢ ( ( ∃ 𝑥 ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) ↔ ( 𝑎 ∈ 𝐴 → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
27 20 26 bitri ⊢ ( ∀ 𝑥 ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) ↔ ( 𝑎 ∈ 𝐴 → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
28 27 albii ⊢ ( ∀ 𝑎 ∀ 𝑥 ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) ↔ ∀ 𝑎 ( 𝑎 ∈ 𝐴 → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
29 alcom ⊢ ( ∀ 𝑥 ∀ 𝑎 ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) ↔ ∀ 𝑎 ∀ 𝑥 ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
30 df-ral ⊢ ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ↔ ∀ 𝑎 ( 𝑎 ∈ 𝐴 → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) )
31 28 29 30 3bitr4i ⊢ ( ∀ 𝑥 ∀ 𝑎 ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 = ( 𝑎 “ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 ) ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
32 19 31 bitri ⊢ ( ∀ 𝑥 ( ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
33 4 32 bitri ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } 𝑦 ∈ 𝑧 ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )
34 2 33 bitri ⊢ ( 𝑦 ∈ ∩ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = ( 𝑎 “ 𝐵 ) } ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ⟨ 𝑏 , 𝑦 ⟩ ∈ 𝑎 )