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

Metamath Proof Explorer

Theorem dfiun2g

Description: Alternate definition of indexed union when B is a set. Definition 15(a) of Suppes p. 44. (Contributed by NM, 23-Mar-2006) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by Rohan Ridenour, 11-Aug-2023) Avoid ax-10 , ax-12 . (Revised by SN, 11-Dec-2024)

Ref Expression
Assertion dfiun2g ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )

Proof

Step Hyp Ref Expression
1 df-iun ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 }
2 elisset ⊢ ( 𝐵 ∈ 𝐶 → ∃ 𝑧 𝑧 = 𝐵 )
3 eleq2 ⊢ ( 𝑧 = 𝐵 → ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝐵 ) )
4 3 pm5.32ri ⊢ ( ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ↔ ( 𝑤 ∈ 𝐵 ∧ 𝑧 = 𝐵 ) )
5 4 simplbi2 ⊢ ( 𝑤 ∈ 𝐵 → ( 𝑧 = 𝐵 → ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) )
6 5 eximdv ⊢ ( 𝑤 ∈ 𝐵 → ( ∃ 𝑧 𝑧 = 𝐵 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) )
7 2 6 syl5com ⊢ ( 𝐵 ∈ 𝐶 → ( 𝑤 ∈ 𝐵 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) )
8 7 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∀ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝐵 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) )
9 rexim ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝐵 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) )
10 8 9 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ) )
11 rexcom4 ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ↔ ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) )
12 r19.42v ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ↔ ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
13 12 exbii ⊢ ( ∃ 𝑧 ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
14 11 13 bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
15 10 14 imbitrdi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 → ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) ) )
16 3 biimpac ⊢ ( ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) → 𝑤 ∈ 𝐵 )
17 16 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑤 ∈ 𝑧 ∧ 𝑧 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 )
18 12 17 sylbir ⊢ ( ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 )
19 18 exlimiv ⊢ ( ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 )
20 15 19 impbid1 ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) ) )
21 vex ⊢ 𝑤 ∈ V
22 eleq1w ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵 ) )
23 22 rexbidv ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ) )
24 21 23 elab ⊢ ( 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 )
25 eluni ⊢ ( 𝑤 ∈ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) )
26 vex ⊢ 𝑧 ∈ V
27 eqeq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 = 𝐵 ↔ 𝑧 = 𝐵 ) )
28 27 rexbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
29 26 28 elab ⊢ ( 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 )
30 29 anbi2i ⊢ ( ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) ↔ ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
31 30 exbii ⊢ ( ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ 𝑧 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
32 25 31 bitri ⊢ ( 𝑤 ∈ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑧 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 ) )
33 20 24 32 3bitr4g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ( 𝑤 ∈ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } ↔ 𝑤 ∈ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } ) )
34 33 eqrdv ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
35 1 34 eqtrid ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )