MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fntpb Structured version   Visualization version   GIF version

Theorem fntpb 7159
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.)
Hypotheses
Ref Expression
fnprb.a 𝐴 ∈ V
fnprb.b 𝐵 ∈ V
fntpb.c 𝐶 ∈ V
Assertion
Ref Expression
fntpb (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})

Proof of Theorem fntpb
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 fnprb.a . . . . . . . 8 𝐴 ∈ V
2 fnprb.b . . . . . . . 8 𝐵 ∈ V
31, 2fnprb 7158 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩})
4 tpidm23 4718 . . . . . . . . 9 {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵}
54eqcomi 2745 . . . . . . . 8 {𝐴, 𝐵} = {𝐴, 𝐵, 𝐵}
65fneq2i 6600 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐵})
7 tpidm23 4718 . . . . . . . . 9 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩}
87eqcomi 2745 . . . . . . . 8 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩}
98eqeq2i 2749 . . . . . . 7 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩})
103, 6, 93bitr3i 300 . . . . . 6 (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩})
1110a1i 11 . . . . 5 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩}))
12 tpeq3 4705 . . . . . 6 (𝐵 = 𝐶 → {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵, 𝐶})
1312fneq2d 6596 . . . . 5 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
14 id 22 . . . . . . . 8 (𝐵 = 𝐶𝐵 = 𝐶)
15 fveq2 6842 . . . . . . . 8 (𝐵 = 𝐶 → (𝐹𝐵) = (𝐹𝐶))
1614, 15opeq12d 4838 . . . . . . 7 (𝐵 = 𝐶 → ⟨𝐵, (𝐹𝐵)⟩ = ⟨𝐶, (𝐹𝐶)⟩)
1716tpeq3d 4708 . . . . . 6 (𝐵 = 𝐶 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
1817eqeq2d 2747 . . . . 5 (𝐵 = 𝐶 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
1911, 13, 183bitr3d 308 . . . 4 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
2019a1d 25 . . 3 (𝐵 = 𝐶 → ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})))
21 fndm 6605 . . . . . . . 8 (𝐹 Fn {𝐴, 𝐵, 𝐶} → dom 𝐹 = {𝐴, 𝐵, 𝐶})
22 fvex 6855 . . . . . . . . 9 (𝐹𝐴) ∈ V
23 fvex 6855 . . . . . . . . 9 (𝐹𝐵) ∈ V
24 fvex 6855 . . . . . . . . 9 (𝐹𝐶) ∈ V
2522, 23, 24dmtpop 6170 . . . . . . . 8 dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {𝐴, 𝐵, 𝐶}
2621, 25eqtr4di 2794 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵, 𝐶} → dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
2726adantl 482 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
2821adantl 482 . . . . . . . . 9 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → dom 𝐹 = {𝐴, 𝐵, 𝐶})
2928eleq2d 2823 . . . . . . . 8 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ dom 𝐹𝑥 ∈ {𝐴, 𝐵, 𝐶}))
30 vex 3449 . . . . . . . . . 10 𝑥 ∈ V
3130eltp 4649 . . . . . . . . 9 (𝑥 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶))
321, 22fvtp1 7144 . . . . . . . . . . . . 13 ((𝐴𝐵𝐴𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴) = (𝐹𝐴))
3332ad2antrr 724 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴) = (𝐹𝐴))
3433eqcomd 2742 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐴) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴))
35 fveq2 6842 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
36 fveq2 6842 . . . . . . . . . . . 12 (𝑥 = 𝐴 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴))
3735, 36eqeq12d 2752 . . . . . . . . . . 11 (𝑥 = 𝐴 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐴) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴)))
3834, 37syl5ibrcom 246 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐴 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
392, 23fvtp2 7145 . . . . . . . . . . . . 13 ((𝐴𝐵𝐵𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵) = (𝐹𝐵))
4039ad4ant13 749 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵) = (𝐹𝐵))
4140eqcomd 2742 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐵) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵))
42 fveq2 6842 . . . . . . . . . . . 12 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
43 fveq2 6842 . . . . . . . . . . . 12 (𝑥 = 𝐵 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵))
4442, 43eqeq12d 2752 . . . . . . . . . . 11 (𝑥 = 𝐵 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐵) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵)))
4541, 44syl5ibrcom 246 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐵 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
46 fntpb.c . . . . . . . . . . . . . 14 𝐶 ∈ V
4746, 24fvtp3 7146 . . . . . . . . . . . . 13 ((𝐴𝐶𝐵𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶) = (𝐹𝐶))
4847ad4ant23 751 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶) = (𝐹𝐶))
4948eqcomd 2742 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐶) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶))
50 fveq2 6842 . . . . . . . . . . . 12 (𝑥 = 𝐶 → (𝐹𝑥) = (𝐹𝐶))
51 fveq2 6842 . . . . . . . . . . . 12 (𝑥 = 𝐶 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶))
5250, 51eqeq12d 2752 . . . . . . . . . . 11 (𝑥 = 𝐶 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐶) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶)))
5349, 52syl5ibrcom 246 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐶 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5438, 45, 533jaod 1428 . . . . . . . . 9 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5531, 54biimtrid 241 . . . . . . . 8 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5629, 55sylbid 239 . . . . . . 7 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ dom 𝐹 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5756ralrimiv 3142 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))
58 fnfun 6602 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵, 𝐶} → Fun 𝐹)
591, 2, 46, 22, 23, 24funtp 6558 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
60593expa 1118 . . . . . . 7 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
61 eqfunfv 6987 . . . . . . 7 ((Fun 𝐹 ∧ Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}) → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))))
6258, 60, 61syl2anr 597 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))))
6327, 57, 62mpbir2and 711 . . . . 5 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
641, 2, 46, 22, 23, 24fntp 6562 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶})
65643expa 1118 . . . . . 6 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶})
66 fneq1 6593 . . . . . . 7 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶}))
6766biimprd 247 . . . . . 6 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶} → 𝐹 Fn {𝐴, 𝐵, 𝐶}))
6865, 67mpan9 507 . . . . 5 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}) → 𝐹 Fn {𝐴, 𝐵, 𝐶})
6963, 68impbida 799 . . . 4 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
7069expcom 414 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})))
7120, 70pm2.61ine 3028 . 2 ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
721, 46fnprb 7158 . . . . 5 (𝐹 Fn {𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
73 tpidm12 4716 . . . . . . 7 {𝐴, 𝐴, 𝐶} = {𝐴, 𝐶}
7473eqcomi 2745 . . . . . 6 {𝐴, 𝐶} = {𝐴, 𝐴, 𝐶}
7574fneq2i 6600 . . . . 5 (𝐹 Fn {𝐴, 𝐶} ↔ 𝐹 Fn {𝐴, 𝐴, 𝐶})
76 tpidm12 4716 . . . . . . 7 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}
7776eqcomi 2745 . . . . . 6 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}
7877eqeq2i 2749 . . . . 5 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
7972, 75, 783bitr3i 300 . . . 4 (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
8079a1i 11 . . 3 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
81 tpeq2 4704 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐴, 𝐶} = {𝐴, 𝐵, 𝐶})
8281fneq2d 6596 . . 3 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
83 id 22 . . . . . 6 (𝐴 = 𝐵𝐴 = 𝐵)
84 fveq2 6842 . . . . . 6 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
8583, 84opeq12d 4838 . . . . 5 (𝐴 = 𝐵 → ⟨𝐴, (𝐹𝐴)⟩ = ⟨𝐵, (𝐹𝐵)⟩)
8685tpeq2d 4707 . . . 4 (𝐴 = 𝐵 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
8786eqeq2d 2747 . . 3 (𝐴 = 𝐵 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
8880, 82, 873bitr3d 308 . 2 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
89 tpidm13 4717 . . . . . . 7 {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵}
9089eqcomi 2745 . . . . . 6 {𝐴, 𝐵} = {𝐴, 𝐵, 𝐴}
9190fneq2i 6600 . . . . 5 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐴})
92 tpidm13 4717 . . . . . . 7 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩}
9392eqcomi 2745 . . . . . 6 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩}
9493eqeq2i 2749 . . . . 5 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩})
953, 91, 943bitr3i 300 . . . 4 (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩})
9695a1i 11 . . 3 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩}))
97 tpeq3 4705 . . . 4 (𝐴 = 𝐶 → {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵, 𝐶})
9897fneq2d 6596 . . 3 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
99 id 22 . . . . . 6 (𝐴 = 𝐶𝐴 = 𝐶)
100 fveq2 6842 . . . . . 6 (𝐴 = 𝐶 → (𝐹𝐴) = (𝐹𝐶))
10199, 100opeq12d 4838 . . . . 5 (𝐴 = 𝐶 → ⟨𝐴, (𝐹𝐴)⟩ = ⟨𝐶, (𝐹𝐶)⟩)
102101tpeq3d 4708 . . . 4 (𝐴 = 𝐶 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
103102eqeq2d 2747 . . 3 (𝐴 = 𝐶 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
10496, 98, 1033bitr3d 308 . 2 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
10571, 88, 104pm2.61iine 3035 1 (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3o 1086   = wceq 1541  wcel 2106  wne 2943  wral 3064  Vcvv 3445  {cpr 4588  {ctp 4590  cop 4592  dom cdm 5633  Fun wfun 6490   Fn wfn 6491  cfv 6496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504
This theorem is referenced by:  wrd3tpop  14837
  Copyright terms: Public domain W3C validator