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

Metamath Proof Explorer

Theorem fntpb

Description: A function whose domain has at most three elements can be represented as a set of at most three ordered pairs. (Contributed by AV, 26-Jan-2021)

Ref Expression
Hypotheses fnprb.a ⊢ 𝐴 ∈ V
fnprb.b ⊢ 𝐵 ∈ V
fntpb.c ⊢ 𝐶 ∈ V
Assertion fntpb ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )

Proof

Step Hyp Ref Expression
1 fnprb.a ⊢ 𝐴 ∈ V
2 fnprb.b ⊢ 𝐵 ∈ V
3 fntpb.c ⊢ 𝐶 ∈ V
4 1 2 fnprb ⊢ ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
5 tpidm23 ⊢ { 𝐴 , 𝐵 , 𝐵 } = { 𝐴 , 𝐵 }
6 5 eqcomi ⊢ { 𝐴 , 𝐵 } = { 𝐴 , 𝐵 , 𝐵 }
7 6 fneq2i ⊢ ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ 𝐹 Fn { 𝐴 , 𝐵 , 𝐵 } )
8 tpidm23 ⊢ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ }
9 8 eqcomi ⊢ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ }
10 9 eqeq2i ⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
11 4 7 10 3bitr3i ⊢ ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } )
12 11 a1i ⊢ ( 𝐵 = 𝐶 → ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐵 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ) )
13 tpeq3 ⊢ ( 𝐵 = 𝐶 → { 𝐴 , 𝐵 , 𝐵 } = { 𝐴 , 𝐵 , 𝐶 } )
14 13 fneq2d ⊢ ( 𝐵 = 𝐶 → ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐵 } ↔ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) )
15 id ⊢ ( 𝐵 = 𝐶 → 𝐵 = 𝐶 )
16 fveq2 ⊢ ( 𝐵 = 𝐶 → ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) )
17 15 16 opeq12d ⊢ ( 𝐵 = 𝐶 → ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ = ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ )
18 17 tpeq3d ⊢ ( 𝐵 = 𝐶 → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )
19 18 eqeq2d ⊢ ( 𝐵 = 𝐶 → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) )
20 12 14 19 3bitr3d ⊢ ( 𝐵 = 𝐶 → ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) )
21 20 a1d ⊢ ( 𝐵 = 𝐶 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) ) )
22 fndm ⊢ ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } → dom 𝐹 = { 𝐴 , 𝐵 , 𝐶 } )
23 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
24 fvex ⊢ ( 𝐹 ‘ 𝐵 ) ∈ V
25 fvex ⊢ ( 𝐹 ‘ 𝐶 ) ∈ V
26 23 24 25 dmtpop ⊢ dom { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } = { 𝐴 , 𝐵 , 𝐶 }
27 22 26 eqtr4di ⊢ ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } → dom 𝐹 = dom { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )
28 27 adantl ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → dom 𝐹 = dom { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )
29 22 adantl ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → dom 𝐹 = { 𝐴 , 𝐵 , 𝐶 } )
30 29 eleq2d ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ) )
31 vex ⊢ 𝑥 ∈ V
32 31 eltp ⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) )
33 1 23 fvtp1 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
34 33 ad2antrr ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
35 34 eqcomd ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝐹 ‘ 𝐴 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐴 ) )
36 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
37 fveq2 ⊢ ( 𝑥 = 𝐴 → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐴 ) )
38 36 37 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐴 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐴 ) ) )
39 35 38 syl5ibrcom ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) ) )
40 2 24 fvtp2 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )
41 40 ad4ant13 ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) )
42 41 eqcomd ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝐹 ‘ 𝐵 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐵 ) )
43 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
44 fveq2 ⊢ ( 𝑥 = 𝐵 → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐵 ) )
45 43 44 eqeq12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐵 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐵 ) ) )
46 42 45 syl5ibrcom ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) ) )
47 3 25 fvtp3 ⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐶 ) = ( 𝐹 ‘ 𝐶 ) )
48 47 ad4ant23 ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐶 ) = ( 𝐹 ‘ 𝐶 ) )
49 48 eqcomd ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝐹 ‘ 𝐶 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐶 ) )
50 fveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐶 ) )
51 fveq2 ⊢ ( 𝑥 = 𝐶 → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐶 ) )
52 50 51 eqeq12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐶 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝐶 ) ) )
53 49 52 syl5ibrcom ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝑥 = 𝐶 → ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) ) )
54 39 46 53 3jaod ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) ) )
55 32 54 biimtrid ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝑥 ∈ { 𝐴 , 𝐵 , 𝐶 } → ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) ) )
56 30 55 sylbid ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝑥 ∈ dom 𝐹 → ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) ) )
57 56 ralrimiv ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ∀ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) )
58 fnfun ⊢ ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } → Fun 𝐹 )
59 1 2 3 23 24 25 funtp ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → Fun { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )
60 59 3expa ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → Fun { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )
61 eqfunfv ⊢ ( ( Fun 𝐹 ∧ Fun { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ↔ ( dom 𝐹 = dom { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ∧ ∀ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) ) ) )
62 58 60 61 syl2anr ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ↔ ( dom 𝐹 = dom { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ∧ ∀ 𝑥 ∈ dom 𝐹 ( 𝐹 ‘ 𝑥 ) = ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ‘ 𝑥 ) ) ) )
63 28 57 62 mpbir2and ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) → 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )
64 1 2 3 23 24 25 fntp ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } Fn { 𝐴 , 𝐵 , 𝐶 } )
65 64 3expa ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } Fn { 𝐴 , 𝐵 , 𝐶 } )
66 fneq1 ⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } → ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } Fn { 𝐴 , 𝐵 , 𝐶 } ) )
67 66 biimprd ⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } → ( { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } Fn { 𝐴 , 𝐵 , 𝐶 } → 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) )
68 65 67 mpan9 ⊢ ( ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) → 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } )
69 63 68 impbida ⊢ ( ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ 𝐵 ≠ 𝐶 ) → ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) )
70 69 expcom ⊢ ( 𝐵 ≠ 𝐶 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) ) )
71 21 70 pm2.61ine ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) )
72 1 3 fnprb ⊢ ( 𝐹 Fn { 𝐴 , 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )
73 tpidm12 ⊢ { 𝐴 , 𝐴 , 𝐶 } = { 𝐴 , 𝐶 }
74 73 eqcomi ⊢ { 𝐴 , 𝐶 } = { 𝐴 , 𝐴 , 𝐶 }
75 74 fneq2i ⊢ ( 𝐹 Fn { 𝐴 , 𝐶 } ↔ 𝐹 Fn { 𝐴 , 𝐴 , 𝐶 } )
76 tpidm12 ⊢ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ }
77 76 eqcomi ⊢ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ }
78 77 eqeq2i ⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )
79 72 75 78 3bitr3i ⊢ ( 𝐹 Fn { 𝐴 , 𝐴 , 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )
80 79 a1i ⊢ ( 𝐴 = 𝐵 → ( 𝐹 Fn { 𝐴 , 𝐴 , 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) )
81 tpeq2 ⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐴 , 𝐶 } = { 𝐴 , 𝐵 , 𝐶 } )
82 81 fneq2d ⊢ ( 𝐴 = 𝐵 → ( 𝐹 Fn { 𝐴 , 𝐴 , 𝐶 } ↔ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) )
83 id ⊢ ( 𝐴 = 𝐵 → 𝐴 = 𝐵 )
84 fveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐵 ) )
85 83 84 opeq12d ⊢ ( 𝐴 = 𝐵 → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ = ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ )
86 85 tpeq2d ⊢ ( 𝐴 = 𝐵 → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )
87 86 eqeq2d ⊢ ( 𝐴 = 𝐵 → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) )
88 80 82 87 3bitr3d ⊢ ( 𝐴 = 𝐵 → ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) )
89 tpidm13 ⊢ { 𝐴 , 𝐵 , 𝐴 } = { 𝐴 , 𝐵 }
90 89 eqcomi ⊢ { 𝐴 , 𝐵 } = { 𝐴 , 𝐵 , 𝐴 }
91 90 fneq2i ⊢ ( 𝐹 Fn { 𝐴 , 𝐵 } ↔ 𝐹 Fn { 𝐴 , 𝐵 , 𝐴 } )
92 tpidm13 ⊢ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ }
93 92 eqcomi ⊢ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ }
94 93 eqeq2i ⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
95 4 91 94 3bitr3i ⊢ ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
96 95 a1i ⊢ ( 𝐴 = 𝐶 → ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐴 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )
97 tpeq3 ⊢ ( 𝐴 = 𝐶 → { 𝐴 , 𝐵 , 𝐴 } = { 𝐴 , 𝐵 , 𝐶 } )
98 97 fneq2d ⊢ ( 𝐴 = 𝐶 → ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐴 } ↔ 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ) )
99 id ⊢ ( 𝐴 = 𝐶 → 𝐴 = 𝐶 )
100 fveq2 ⊢ ( 𝐴 = 𝐶 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) )
101 99 100 opeq12d ⊢ ( 𝐴 = 𝐶 → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ = ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ )
102 101 tpeq3d ⊢ ( 𝐴 = 𝐶 → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )
103 102 eqeq2d ⊢ ( 𝐴 = 𝐶 → ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) )
104 96 98 103 3bitr3d ⊢ ( 𝐴 = 𝐶 → ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } ) )
105 71 88 104 pm2.61iine ⊢ ( 𝐹 Fn { 𝐴 , 𝐵 , 𝐶 } ↔ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ , ⟨ 𝐵 , ( 𝐹 ‘ 𝐵 ) ⟩ , ⟨ 𝐶 , ( 𝐹 ‘ 𝐶 ) ⟩ } )