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 ( ∀ 𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } )