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

Theorem fntpb 6964
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 6963 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩})
4 tpidm23 4687 . . . . . . . . 9 {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵}
54eqcomi 2830 . . . . . . . 8 {𝐴, 𝐵} = {𝐴, 𝐵, 𝐵}
65fneq2i 6445 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐵})
7 tpidm23 4687 . . . . . . . . 9 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩}
87eqcomi 2830 . . . . . . . 8 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩}
98eqeq2i 2834 . . . . . . 7 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩})
103, 6, 93bitr3i 302 . . . . . 6 (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩})
1110a1i 11 . . . . 5 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩}))
12 tpeq3 4674 . . . . . 6 (𝐵 = 𝐶 → {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵, 𝐶})
1312fneq2d 6441 . . . . 5 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
14 id 22 . . . . . . . 8 (𝐵 = 𝐶𝐵 = 𝐶)
15 fveq2 6664 . . . . . . . 8 (𝐵 = 𝐶 → (𝐹𝐵) = (𝐹𝐶))
1614, 15opeq12d 4805 . . . . . . 7 (𝐵 = 𝐶 → ⟨𝐵, (𝐹𝐵)⟩ = ⟨𝐶, (𝐹𝐶)⟩)
1716tpeq3d 4677 . . . . . 6 (𝐵 = 𝐶 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
1817eqeq2d 2832 . . . . 5 (𝐵 = 𝐶 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
1911, 13, 183bitr3d 310 . . . 4 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
2019a1d 25 . . 3 (𝐵 = 𝐶 → ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})))
21 fndm 6449 . . . . . . . 8 (𝐹 Fn {𝐴, 𝐵, 𝐶} → dom 𝐹 = {𝐴, 𝐵, 𝐶})
22 fvex 6677 . . . . . . . . 9 (𝐹𝐴) ∈ V
23 fvex 6677 . . . . . . . . 9 (𝐹𝐵) ∈ V
24 fvex 6677 . . . . . . . . 9 (𝐹𝐶) ∈ V
2522, 23, 24dmtpop 6069 . . . . . . . 8 dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {𝐴, 𝐵, 𝐶}
2621, 25syl6eqr 2874 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵, 𝐶} → dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
2726adantl 482 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
2821adantl 482 . . . . . . . . 9 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → dom 𝐹 = {𝐴, 𝐵, 𝐶})
2928eleq2d 2898 . . . . . . . 8 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ dom 𝐹𝑥 ∈ {𝐴, 𝐵, 𝐶}))
30 vex 3498 . . . . . . . . . 10 𝑥 ∈ V
3130eltp 4620 . . . . . . . . 9 (𝑥 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶))
321, 22fvtp1 6950 . . . . . . . . . . . . 13 ((𝐴𝐵𝐴𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴) = (𝐹𝐴))
3332ad2antrr 722 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴) = (𝐹𝐴))
3433eqcomd 2827 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐴) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴))
35 fveq2 6664 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
36 fveq2 6664 . . . . . . . . . . . 12 (𝑥 = 𝐴 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴))
3735, 36eqeq12d 2837 . . . . . . . . . . 11 (𝑥 = 𝐴 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐴) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴)))
3834, 37syl5ibrcom 248 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐴 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
392, 23fvtp2 6951 . . . . . . . . . . . . 13 ((𝐴𝐵𝐵𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵) = (𝐹𝐵))
4039ad4ant13 747 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵) = (𝐹𝐵))
4140eqcomd 2827 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐵) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵))
42 fveq2 6664 . . . . . . . . . . . 12 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
43 fveq2 6664 . . . . . . . . . . . 12 (𝑥 = 𝐵 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵))
4442, 43eqeq12d 2837 . . . . . . . . . . 11 (𝑥 = 𝐵 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐵) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵)))
4541, 44syl5ibrcom 248 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐵 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
46 fntpb.c . . . . . . . . . . . . . 14 𝐶 ∈ V
4746, 24fvtp3 6952 . . . . . . . . . . . . 13 ((𝐴𝐶𝐵𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶) = (𝐹𝐶))
4847ad4ant23 749 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶) = (𝐹𝐶))
4948eqcomd 2827 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐶) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶))
50 fveq2 6664 . . . . . . . . . . . 12 (𝑥 = 𝐶 → (𝐹𝑥) = (𝐹𝐶))
51 fveq2 6664 . . . . . . . . . . . 12 (𝑥 = 𝐶 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶))
5250, 51eqeq12d 2837 . . . . . . . . . . 11 (𝑥 = 𝐶 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐶) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶)))
5349, 52syl5ibrcom 248 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐶 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5438, 45, 533jaod 1420 . . . . . . . . 9 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5531, 54syl5bi 243 . . . . . . . 8 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5629, 55sylbid 241 . . . . . . 7 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ dom 𝐹 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5756ralrimiv 3181 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))
58 fnfun 6447 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵, 𝐶} → Fun 𝐹)
591, 2, 46, 22, 23, 24funtp 6405 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
60593expa 1110 . . . . . . 7 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
61 eqfunfv 6800 . . . . . . 7 ((Fun 𝐹 ∧ Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}) → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))))
6258, 60, 61syl2anr 596 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))))
6327, 57, 62mpbir2and 709 . . . . 5 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
641, 2, 46, 22, 23, 24fntp 6409 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶})
65643expa 1110 . . . . . 6 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶})
66 fneq1 6438 . . . . . . 7 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶}))
6766biimprd 249 . . . . . 6 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶} → 𝐹 Fn {𝐴, 𝐵, 𝐶}))
6865, 67mpan9 507 . . . . 5 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}) → 𝐹 Fn {𝐴, 𝐵, 𝐶})
6963, 68impbida 797 . . . 4 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
7069expcom 414 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})))
7120, 70pm2.61ine 3100 . 2 ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
721, 46fnprb 6963 . . . . 5 (𝐹 Fn {𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
73 tpidm12 4685 . . . . . . 7 {𝐴, 𝐴, 𝐶} = {𝐴, 𝐶}
7473eqcomi 2830 . . . . . 6 {𝐴, 𝐶} = {𝐴, 𝐴, 𝐶}
7574fneq2i 6445 . . . . 5 (𝐹 Fn {𝐴, 𝐶} ↔ 𝐹 Fn {𝐴, 𝐴, 𝐶})
76 tpidm12 4685 . . . . . . 7 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}
7776eqcomi 2830 . . . . . 6 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}
7877eqeq2i 2834 . . . . 5 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
7972, 75, 783bitr3i 302 . . . 4 (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
8079a1i 11 . . 3 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
81 tpeq2 4673 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐴, 𝐶} = {𝐴, 𝐵, 𝐶})
8281fneq2d 6441 . . 3 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
83 id 22 . . . . . 6 (𝐴 = 𝐵𝐴 = 𝐵)
84 fveq2 6664 . . . . . 6 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
8583, 84opeq12d 4805 . . . . 5 (𝐴 = 𝐵 → ⟨𝐴, (𝐹𝐴)⟩ = ⟨𝐵, (𝐹𝐵)⟩)
8685tpeq2d 4676 . . . 4 (𝐴 = 𝐵 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
8786eqeq2d 2832 . . 3 (𝐴 = 𝐵 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
8880, 82, 873bitr3d 310 . 2 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
89 tpidm13 4686 . . . . . . 7 {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵}
9089eqcomi 2830 . . . . . 6 {𝐴, 𝐵} = {𝐴, 𝐵, 𝐴}
9190fneq2i 6445 . . . . 5 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐴})
92 tpidm13 4686 . . . . . . 7 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩}
9392eqcomi 2830 . . . . . 6 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩}
9493eqeq2i 2834 . . . . 5 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩})
953, 91, 943bitr3i 302 . . . 4 (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩})
9695a1i 11 . . 3 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩}))
97 tpeq3 4674 . . . 4 (𝐴 = 𝐶 → {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵, 𝐶})
9897fneq2d 6441 . . 3 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
99 id 22 . . . . . 6 (𝐴 = 𝐶𝐴 = 𝐶)
100 fveq2 6664 . . . . . 6 (𝐴 = 𝐶 → (𝐹𝐴) = (𝐹𝐶))
10199, 100opeq12d 4805 . . . . 5 (𝐴 = 𝐶 → ⟨𝐴, (𝐹𝐴)⟩ = ⟨𝐶, (𝐹𝐶)⟩)
102101tpeq3d 4677 . . . 4 (𝐴 = 𝐶 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
103102eqeq2d 2832 . . 3 (𝐴 = 𝐶 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
10496, 98, 1033bitr3d 310 . 2 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
10571, 88, 104pm2.61iine 3107 1 (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3o 1078   = wceq 1528  wcel 2105  wne 3016  wral 3138  Vcvv 3495  {cpr 4561  {ctp 4563  cop 4565  dom cdm 5549  Fun wfun 6343   Fn wfn 6344  cfv 6349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357
This theorem is referenced by:  wrd3tpop  14300
  Copyright terms: Public domain W3C validator