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

Metamath Proof Explorer

Theorem dfiota3

Description: A definition of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013)

Ref Expression
Assertion dfiota3 ( ℩ 𝑥 𝜑 ) = ∪ ∪ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons )

Proof

Step Hyp Ref Expression
1 df-iota ⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } }
2 eqabcb ⊢ ( { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } ↔ ∀ 𝑦 ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ 𝑦 ∈ ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } ) )
3 exdistr ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
4 vex ⊢ 𝑦 ∈ V
5 sneq ⊢ ( 𝑤 = 𝑦 → { 𝑤 } = { 𝑦 } )
6 5 eqeq2d ⊢ ( 𝑤 = 𝑦 → ( { 𝑥 ∣ 𝜑 } = { 𝑤 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑦 } ) )
7 4 6 ceqsexv ⊢ ( ∃ 𝑤 ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) ↔ { 𝑥 ∣ 𝜑 } = { 𝑦 } )
8 vsnex ⊢ { 𝑤 } ∈ V
9 eqeq1 ⊢ ( 𝑧 = { 𝑤 } → ( 𝑧 = { 𝑥 ∣ 𝜑 } ↔ { 𝑤 } = { 𝑥 ∣ 𝜑 } ) )
10 eleq2 ⊢ ( 𝑧 = { 𝑤 } → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ { 𝑤 } ) )
11 9 10 anbi12d ⊢ ( 𝑧 = { 𝑤 } → ( ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝑧 ) ↔ ( { 𝑤 } = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ { 𝑤 } ) ) )
12 eqcom ⊢ ( { 𝑤 } = { 𝑥 ∣ 𝜑 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑤 } )
13 velsn ⊢ ( 𝑦 ∈ { 𝑤 } ↔ 𝑦 = 𝑤 )
14 equcom ⊢ ( 𝑦 = 𝑤 ↔ 𝑤 = 𝑦 )
15 13 14 bitri ⊢ ( 𝑦 ∈ { 𝑤 } ↔ 𝑤 = 𝑦 )
16 12 15 anbi12ci ⊢ ( ( { 𝑤 } = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ { 𝑤 } ) ↔ ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) )
17 11 16 bitrdi ⊢ ( 𝑧 = { 𝑤 } → ( ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝑧 ) ↔ ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) ) )
18 8 17 ceqsexv ⊢ ( ∃ 𝑧 ( 𝑧 = { 𝑤 } ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝑧 ) ) ↔ ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) )
19 an13 ⊢ ( ( 𝑧 = { 𝑤 } ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝑧 ) ) ↔ ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
20 19 exbii ⊢ ( ∃ 𝑧 ( 𝑧 = { 𝑤 } ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝑧 ) ) ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
21 18 20 bitr3i ⊢ ( ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
22 21 exbii ⊢ ( ∃ 𝑤 ( 𝑤 = 𝑦 ∧ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) ↔ ∃ 𝑤 ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
23 7 22 bitr3i ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∃ 𝑤 ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
24 excom ⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
25 23 24 bitri ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑦 ∈ 𝑧 ∧ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
26 eluniab ⊢ ( 𝑦 ∈ ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ) )
27 3 25 26 3bitr4i ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ 𝑦 ∈ ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) } )
28 2 27 mpgbir ⊢ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) }
29 df-sn ⊢ { { 𝑥 ∣ 𝜑 } } = { 𝑧 ∣ 𝑧 = { 𝑥 ∣ 𝜑 } }
30 dfsingles2 ⊢ Singletons = { 𝑧 ∣ ∃ 𝑤 𝑧 = { 𝑤 } }
31 29 30 ineq12i ⊢ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons ) = ( { 𝑧 ∣ 𝑧 = { 𝑥 ∣ 𝜑 } } ∩ { 𝑧 ∣ ∃ 𝑤 𝑧 = { 𝑤 } } )
32 inab ⊢ ( { 𝑧 ∣ 𝑧 = { 𝑥 ∣ 𝜑 } } ∩ { 𝑧 ∣ ∃ 𝑤 𝑧 = { 𝑤 } } ) = { 𝑧 ∣ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ ∃ 𝑤 𝑧 = { 𝑤 } ) }
33 19.42v ⊢ ( ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) ↔ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ ∃ 𝑤 𝑧 = { 𝑤 } ) )
34 33 bicomi ⊢ ( ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ ∃ 𝑤 𝑧 = { 𝑤 } ) ↔ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) )
35 34 abbii ⊢ { 𝑧 ∣ ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ ∃ 𝑤 𝑧 = { 𝑤 } ) } = { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) }
36 32 35 eqtri ⊢ ( { 𝑧 ∣ 𝑧 = { 𝑥 ∣ 𝜑 } } ∩ { 𝑧 ∣ ∃ 𝑤 𝑧 = { 𝑤 } } ) = { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) }
37 31 36 eqtri ⊢ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons ) = { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) }
38 37 unieqi ⊢ ∪ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons ) = ∪ { 𝑧 ∣ ∃ 𝑤 ( 𝑧 = { 𝑥 ∣ 𝜑 } ∧ 𝑧 = { 𝑤 } ) }
39 28 38 eqtr4i ⊢ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons )
40 39 unieqi ⊢ ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ ∪ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons )
41 1 40 eqtri ⊢ ( ℩ 𝑥 𝜑 ) = ∪ ∪ ( { { 𝑥 ∣ 𝜑 } } ∩ Singletons )