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

Metamath Proof Explorer

Theorem fnimatpd

Description: The image of an unordered triple under a function. (Contributed by Thierry Arnoux, 19-Sep-2023)

Ref Expression
Hypotheses fnimatpd.1 ⊢ φ → F Fn D
fnimatpd.2 ⊢ φ → A ∈ D
fnimatpd.3 ⊢ φ → B ∈ D
fnimatpd.4 ⊢ φ → C ∈ D
Assertion fnimatpd ⊢ φ → F A B C = F ⁡ A F ⁡ B F ⁡ C

Proof

Step Hyp Ref Expression
1 fnimatpd.1 ⊢ φ → F Fn D
2 fnimatpd.2 ⊢ φ → A ∈ D
3 fnimatpd.3 ⊢ φ → B ∈ D
4 fnimatpd.4 ⊢ φ → C ∈ D
5 fnimapr ⊢ F Fn D ∧ A ∈ D ∧ B ∈ D → F A B = F ⁡ A F ⁡ B
6 1 2 3 5 syl3anc ⊢ φ → F A B = F ⁡ A F ⁡ B
7 fnsnfv ⊢ F Fn D ∧ C ∈ D → F ⁡ C = F C
8 1 4 7 syl2anc ⊢ φ → F ⁡ C = F C
9 8 eqcomd ⊢ φ → F C = F ⁡ C
10 6 9 uneq12d ⊢ φ → F A B ∪ F C = F ⁡ A F ⁡ B ∪ F ⁡ C
11 df-tp ⊢ A B C = A B ∪ C
12 11 imaeq2i ⊢ F A B C = F A B ∪ C
13 imaundi ⊢ F A B ∪ C = F A B ∪ F C
14 12 13 eqtri ⊢ F A B C = F A B ∪ F C
15 df-tp ⊢ F ⁡ A F ⁡ B F ⁡ C = F ⁡ A F ⁡ B ∪ F ⁡ C
16 10 14 15 3eqtr4g ⊢ φ → F A B C = F ⁡ A F ⁡ B F ⁡ C