Metamath Proof Explorer

Theorem abfmpunirn

Description: Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 28-Sep-2016)

Ref Expression
Hypotheses abfmpunirn.1 ⊢ F = x ∈ V ⟼ y | φ
abfmpunirn.2 ⊢ y | φ ∈ V
abfmpunirn.3 ⊢ y = B → φ ↔ ψ
Assertion abfmpunirn ⊢ B ∈ ⋃ ran ⁡ F ↔ B ∈ V ∧ ∃ x ∈ V ψ

Proof

Step Hyp Ref Expression
1 abfmpunirn.1 ⊢ F = x ∈ V ⟼ y | φ
2 abfmpunirn.2 ⊢ y | φ ∈ V
3 abfmpunirn.3 ⊢ y = B → φ ↔ ψ
4 elex ⊢ B ∈ ⋃ ran ⁡ F → B ∈ V
5 2 1 fnmpti ⊢ F Fn V
6 fnunirn ⊢ F Fn V → B ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ V B ∈ F ⁡ x
7 5 6 ax-mp ⊢ B ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ V B ∈ F ⁡ x
8 1 fvmpt2 ⊢ x ∈ V ∧ y | φ ∈ V → F ⁡ x = y | φ
9 2 8 mpan2 ⊢ x ∈ V → F ⁡ x = y | φ
10 9 eleq2d ⊢ x ∈ V → B ∈ F ⁡ x ↔ B ∈ y | φ
11 10 rexbiia ⊢ ∃ x ∈ V B ∈ F ⁡ x ↔ ∃ x ∈ V B ∈ y | φ
12 7 11 bitri ⊢ B ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ V B ∈ y | φ
13 3 elabg ⊢ B ∈ V → B ∈ y | φ ↔ ψ
14 13 rexbidv ⊢ B ∈ V → ∃ x ∈ V B ∈ y | φ ↔ ∃ x ∈ V ψ
15 12 14 syl5bb ⊢ B ∈ V → B ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ V ψ
16 4 15 biadanii ⊢ B ∈ ⋃ ran ⁡ F ↔ B ∈ V ∧ ∃ x ∈ V ψ