Metamath Proof Explorer

Theorem elunirn

Description: Membership in the union of the range of a function. See elunirnALT for a shorter proof which uses ax-pow . (Contributed by NM, 24-Sep-2006)

Ref Expression
Assertion elunirn ⊢ Fun ⁡ F → A ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F A ∈ F ⁡ x

Proof

Step Hyp Ref Expression
1 eluni ⊢ A ∈ ⋃ ran ⁡ F ↔ ∃ y A ∈ y ∧ y ∈ ran ⁡ F
2 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
3 fvelrnb ⊢ F Fn dom ⁡ F → y ∈ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F F ⁡ x = y
4 2 3 sylbi ⊢ Fun ⁡ F → y ∈ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F F ⁡ x = y
5 4 anbi2d ⊢ Fun ⁡ F → A ∈ y ∧ y ∈ ran ⁡ F ↔ A ∈ y ∧ ∃ x ∈ dom ⁡ F F ⁡ x = y
6 r19.42v ⊢ ∃ x ∈ dom ⁡ F A ∈ y ∧ F ⁡ x = y ↔ A ∈ y ∧ ∃ x ∈ dom ⁡ F F ⁡ x = y
7 5 6 bitr4di ⊢ Fun ⁡ F → A ∈ y ∧ y ∈ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F A ∈ y ∧ F ⁡ x = y
8 eleq2 ⊢ F ⁡ x = y → A ∈ F ⁡ x ↔ A ∈ y
9 8 biimparc ⊢ A ∈ y ∧ F ⁡ x = y → A ∈ F ⁡ x
10 9 reximi ⊢ ∃ x ∈ dom ⁡ F A ∈ y ∧ F ⁡ x = y → ∃ x ∈ dom ⁡ F A ∈ F ⁡ x
11 7 10 syl6bi ⊢ Fun ⁡ F → A ∈ y ∧ y ∈ ran ⁡ F → ∃ x ∈ dom ⁡ F A ∈ F ⁡ x
12 11 exlimdv ⊢ Fun ⁡ F → ∃ y A ∈ y ∧ y ∈ ran ⁡ F → ∃ x ∈ dom ⁡ F A ∈ F ⁡ x
13 fvelrn ⊢ Fun ⁡ F ∧ x ∈ dom ⁡ F → F ⁡ x ∈ ran ⁡ F
14 13 a1d ⊢ Fun ⁡ F ∧ x ∈ dom ⁡ F → A ∈ F ⁡ x → F ⁡ x ∈ ran ⁡ F
15 14 ancld ⊢ Fun ⁡ F ∧ x ∈ dom ⁡ F → A ∈ F ⁡ x → A ∈ F ⁡ x ∧ F ⁡ x ∈ ran ⁡ F
16 fvex ⊢ F ⁡ x ∈ V
17 eleq2 ⊢ y = F ⁡ x → A ∈ y ↔ A ∈ F ⁡ x
18 eleq1 ⊢ y = F ⁡ x → y ∈ ran ⁡ F ↔ F ⁡ x ∈ ran ⁡ F
19 17 18 anbi12d ⊢ y = F ⁡ x → A ∈ y ∧ y ∈ ran ⁡ F ↔ A ∈ F ⁡ x ∧ F ⁡ x ∈ ran ⁡ F
20 16 19 spcev ⊢ A ∈ F ⁡ x ∧ F ⁡ x ∈ ran ⁡ F → ∃ y A ∈ y ∧ y ∈ ran ⁡ F
21 15 20 syl6 ⊢ Fun ⁡ F ∧ x ∈ dom ⁡ F → A ∈ F ⁡ x → ∃ y A ∈ y ∧ y ∈ ran ⁡ F
22 21 rexlimdva ⊢ Fun ⁡ F → ∃ x ∈ dom ⁡ F A ∈ F ⁡ x → ∃ y A ∈ y ∧ y ∈ ran ⁡ F
23 12 22 impbid ⊢ Fun ⁡ F → ∃ y A ∈ y ∧ y ∈ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F A ∈ F ⁡ x
24 1 23 syl5bb ⊢ Fun ⁡ F → A ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ dom ⁡ F A ∈ F ⁡ x