Description: Equality theorem for the collection operation. (Contributed by Rohan Ridenour, 11-Aug-2023)
Ref | Expression | ||
---|---|---|---|
Hypotheses | colleq12d.1 | ⊢ ( 𝜑 → 𝐹 = 𝐺 ) | |
colleq12d.2 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) | ||
Assertion | colleq12d | ⊢ ( 𝜑 → ( 𝐹 Coll 𝐴 ) = ( 𝐺 Coll 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | colleq12d.1 | ⊢ ( 𝜑 → 𝐹 = 𝐺 ) | |
2 | colleq12d.2 | ⊢ ( 𝜑 → 𝐴 = 𝐵 ) | |
3 | 1 | imaeq1d | ⊢ ( 𝜑 → ( 𝐹 “ { 𝑥 } ) = ( 𝐺 “ { 𝑥 } ) ) |
4 | 3 | scotteqd | ⊢ ( 𝜑 → Scott ( 𝐹 “ { 𝑥 } ) = Scott ( 𝐺 “ { 𝑥 } ) ) |
5 | 2 4 | iuneq12d | ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 Scott ( 𝐹 “ { 𝑥 } ) = ∪ 𝑥 ∈ 𝐵 Scott ( 𝐺 “ { 𝑥 } ) ) |
6 | df-coll | ⊢ ( 𝐹 Coll 𝐴 ) = ∪ 𝑥 ∈ 𝐴 Scott ( 𝐹 “ { 𝑥 } ) | |
7 | df-coll | ⊢ ( 𝐺 Coll 𝐵 ) = ∪ 𝑥 ∈ 𝐵 Scott ( 𝐺 “ { 𝑥 } ) | |
8 | 5 6 7 | 3eqtr4g | ⊢ ( 𝜑 → ( 𝐹 Coll 𝐴 ) = ( 𝐺 Coll 𝐵 ) ) |