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

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 ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∣ 𝜑 } )
abfmpunirn.2 ⊢ { 𝑦 ∣ 𝜑 } ∈ V
abfmpunirn.3 ⊢ ( 𝑦 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
Assertion abfmpunirn ( 𝐵 ∈ ∪ ran 𝐹 ↔ ( 𝐵 ∈ V ∧ ∃ 𝑥 ∈ 𝑉 𝜓 ) )

Proof

Step Hyp Ref Expression
1 abfmpunirn.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∣ 𝜑 } )
2 abfmpunirn.2 ⊢ { 𝑦 ∣ 𝜑 } ∈ V
3 abfmpunirn.3 ⊢ ( 𝑦 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
4 elex ⊢ ( 𝐵 ∈ ∪ ran 𝐹 → 𝐵 ∈ V )
5 2 1 fnmpti ⊢ 𝐹 Fn 𝑉
6 fnunirn ⊢ ( 𝐹 Fn 𝑉 → ( 𝐵 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) ) )
7 5 6 ax-mp ⊢ ( 𝐵 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) )
8 1 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑉 ∧ { 𝑦 ∣ 𝜑 } ∈ V ) → ( 𝐹 ‘ 𝑥 ) = { 𝑦 ∣ 𝜑 } )
9 2 8 mpan2 ⊢ ( 𝑥 ∈ 𝑉 → ( 𝐹 ‘ 𝑥 ) = { 𝑦 ∣ 𝜑 } )
10 9 eleq2d ⊢ ( 𝑥 ∈ 𝑉 → ( 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) ↔ 𝐵 ∈ { 𝑦 ∣ 𝜑 } ) )
11 10 rexbiia ⊢ ( ∃ 𝑥 ∈ 𝑉 𝐵 ∈ ( 𝐹 ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝑉 𝐵 ∈ { 𝑦 ∣ 𝜑 } )
12 7 11 bitri ⊢ ( 𝐵 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 𝐵 ∈ { 𝑦 ∣ 𝜑 } )
13 3 elabg ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜓 ) )
14 13 rexbidv ⊢ ( 𝐵 ∈ V → ( ∃ 𝑥 ∈ 𝑉 𝐵 ∈ { 𝑦 ∣ 𝜑 } ↔ ∃ 𝑥 ∈ 𝑉 𝜓 ) )
15 12 14 bitrid ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 𝜓 ) )
16 4 15 biadanii ⊢ ( 𝐵 ∈ ∪ ran 𝐹 ↔ ( 𝐵 ∈ V ∧ ∃ 𝑥 ∈ 𝑉 𝜓 ) )