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

Theorem fntpb 6638
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 6637 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩})
4 tpidm23 4436 . . . . . . . . 9 {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵}
54eqcomi 2769 . . . . . . . 8 {𝐴, 𝐵} = {𝐴, 𝐵, 𝐵}
65fneq2i 6147 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐵})
7 tpidm23 4436 . . . . . . . . 9 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩}
87eqcomi 2769 . . . . . . . 8 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩}
98eqeq2i 2772 . . . . . . 7 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩})
103, 6, 93bitr3i 290 . . . . . 6 (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩})
1110a1i 11 . . . . 5 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩}))
12 tpeq3 4423 . . . . . 6 (𝐵 = 𝐶 → {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵, 𝐶})
1312fneq2d 6143 . . . . 5 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
14 id 22 . . . . . . . 8 (𝐵 = 𝐶𝐵 = 𝐶)
15 fveq2 6353 . . . . . . . 8 (𝐵 = 𝐶 → (𝐹𝐵) = (𝐹𝐶))
1614, 15opeq12d 4561 . . . . . . 7 (𝐵 = 𝐶 → ⟨𝐵, (𝐹𝐵)⟩ = ⟨𝐶, (𝐹𝐶)⟩)
1716tpeq3d 4426 . . . . . 6 (𝐵 = 𝐶 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
1817eqeq2d 2770 . . . . 5 (𝐵 = 𝐶 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
1911, 13, 183bitr3d 298 . . . 4 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
2019a1d 25 . . 3 (𝐵 = 𝐶 → ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})))
21 fndm 6151 . . . . . . . 8 (𝐹 Fn {𝐴, 𝐵, 𝐶} → dom 𝐹 = {𝐴, 𝐵, 𝐶})
22 fvex 6363 . . . . . . . . 9 (𝐹𝐴) ∈ V
23 fvex 6363 . . . . . . . . 9 (𝐹𝐵) ∈ V
24 fvex 6363 . . . . . . . . 9 (𝐹𝐶) ∈ V
2522, 23, 24dmtpop 5770 . . . . . . . 8 dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {𝐴, 𝐵, 𝐶}
2621, 25syl6eqr 2812 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵, 𝐶} → dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
2726adantl 473 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
2821adantl 473 . . . . . . . . 9 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → dom 𝐹 = {𝐴, 𝐵, 𝐶})
2928eleq2d 2825 . . . . . . . 8 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ dom 𝐹𝑥 ∈ {𝐴, 𝐵, 𝐶}))
30 vex 3343 . . . . . . . . . 10 𝑥 ∈ V
3130eltp 4374 . . . . . . . . 9 (𝑥 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶))
321, 22fvtp1 6625 . . . . . . . . . . . . 13 ((𝐴𝐵𝐴𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴) = (𝐹𝐴))
3332ad2antrr 764 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴) = (𝐹𝐴))
3433eqcomd 2766 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐴) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴))
35 fveq2 6353 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
36 fveq2 6353 . . . . . . . . . . . 12 (𝑥 = 𝐴 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴))
3735, 36eqeq12d 2775 . . . . . . . . . . 11 (𝑥 = 𝐴 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐴) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴)))
3834, 37syl5ibrcom 237 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐴 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
392, 23fvtp2 6626 . . . . . . . . . . . . 13 ((𝐴𝐵𝐵𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵) = (𝐹𝐵))
4039ad4ant13 1207 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵) = (𝐹𝐵))
4140eqcomd 2766 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐵) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵))
42 fveq2 6353 . . . . . . . . . . . 12 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
43 fveq2 6353 . . . . . . . . . . . 12 (𝑥 = 𝐵 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵))
4442, 43eqeq12d 2775 . . . . . . . . . . 11 (𝑥 = 𝐵 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐵) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵)))
4541, 44syl5ibrcom 237 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐵 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
46 fntpb.c . . . . . . . . . . . . . 14 𝐶 ∈ V
4746, 24fvtp3 6627 . . . . . . . . . . . . 13 ((𝐴𝐶𝐵𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶) = (𝐹𝐶))
4847ad4ant23 1211 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶) = (𝐹𝐶))
4948eqcomd 2766 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐶) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶))
50 fveq2 6353 . . . . . . . . . . . 12 (𝑥 = 𝐶 → (𝐹𝑥) = (𝐹𝐶))
51 fveq2 6353 . . . . . . . . . . . 12 (𝑥 = 𝐶 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶))
5250, 51eqeq12d 2775 . . . . . . . . . . 11 (𝑥 = 𝐶 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐶) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶)))
5349, 52syl5ibrcom 237 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐶 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5438, 45, 533jaod 1541 . . . . . . . . 9 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5531, 54syl5bi 232 . . . . . . . 8 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5629, 55sylbid 230 . . . . . . 7 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ dom 𝐹 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5756ralrimiv 3103 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))
58 fnfun 6149 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵, 𝐶} → Fun 𝐹)
591, 2, 46, 22, 23, 24funtp 6106 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
60593expa 1112 . . . . . . 7 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
61 eqfunfv 6480 . . . . . . 7 ((Fun 𝐹 ∧ Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}) → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))))
6258, 60, 61syl2anr 496 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))))
6327, 57, 62mpbir2and 995 . . . . 5 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
641, 2, 46, 22, 23, 24fntp 6110 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶})
65643expa 1112 . . . . . 6 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶})
66 fneq1 6140 . . . . . . 7 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶}))
6766biimprd 238 . . . . . 6 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶} → 𝐹 Fn {𝐴, 𝐵, 𝐶}))
6865, 67mpan9 487 . . . . 5 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}) → 𝐹 Fn {𝐴, 𝐵, 𝐶})
6963, 68impbida 913 . . . 4 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
7069expcom 450 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})))
7120, 70pm2.61ine 3015 . 2 ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
721, 46fnprb 6637 . . . . 5 (𝐹 Fn {𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
73 tpidm12 4434 . . . . . . 7 {𝐴, 𝐴, 𝐶} = {𝐴, 𝐶}
7473eqcomi 2769 . . . . . 6 {𝐴, 𝐶} = {𝐴, 𝐴, 𝐶}
7574fneq2i 6147 . . . . 5 (𝐹 Fn {𝐴, 𝐶} ↔ 𝐹 Fn {𝐴, 𝐴, 𝐶})
76 tpidm12 4434 . . . . . . 7 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}
7776eqcomi 2769 . . . . . 6 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}
7877eqeq2i 2772 . . . . 5 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
7972, 75, 783bitr3i 290 . . . 4 (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
8079a1i 11 . . 3 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
81 tpeq2 4422 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐴, 𝐶} = {𝐴, 𝐵, 𝐶})
8281fneq2d 6143 . . 3 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
83 id 22 . . . . . 6 (𝐴 = 𝐵𝐴 = 𝐵)
84 fveq2 6353 . . . . . 6 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
8583, 84opeq12d 4561 . . . . 5 (𝐴 = 𝐵 → ⟨𝐴, (𝐹𝐴)⟩ = ⟨𝐵, (𝐹𝐵)⟩)
8685tpeq2d 4425 . . . 4 (𝐴 = 𝐵 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
8786eqeq2d 2770 . . 3 (𝐴 = 𝐵 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
8880, 82, 873bitr3d 298 . 2 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
89 tpidm13 4435 . . . . . . 7 {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵}
9089eqcomi 2769 . . . . . 6 {𝐴, 𝐵} = {𝐴, 𝐵, 𝐴}
9190fneq2i 6147 . . . . 5 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐴})
92 tpidm13 4435 . . . . . . 7 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩}
9392eqcomi 2769 . . . . . 6 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩}
9493eqeq2i 2772 . . . . 5 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩})
953, 91, 943bitr3i 290 . . . 4 (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩})
9695a1i 11 . . 3 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩}))
97 tpeq3 4423 . . . 4 (𝐴 = 𝐶 → {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵, 𝐶})
9897fneq2d 6143 . . 3 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
99 id 22 . . . . . 6 (𝐴 = 𝐶𝐴 = 𝐶)
100 fveq2 6353 . . . . . 6 (𝐴 = 𝐶 → (𝐹𝐴) = (𝐹𝐶))
10199, 100opeq12d 4561 . . . . 5 (𝐴 = 𝐶 → ⟨𝐴, (𝐹𝐴)⟩ = ⟨𝐶, (𝐹𝐶)⟩)
102101tpeq3d 4426 . . . 4 (𝐴 = 𝐶 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
103102eqeq2d 2770 . . 3 (𝐴 = 𝐶 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
10496, 98, 1033bitr3d 298 . 2 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
10571, 88, 104pm2.61iine 3022 1 (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3o 1071   = wceq 1632  wcel 2139  wne 2932  wral 3050  Vcvv 3340  {cpr 4323  {ctp 4325  cop 4327  dom cdm 5266  Fun wfun 6043   Fn wfn 6044  cfv 6049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057
This theorem is referenced by:  wrd3tpop  13912
  Copyright terms: Public domain W3C validator