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 𝐹 → ( 𝐴 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )

Proof

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