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

Theorem fntpb 6514
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 6513 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩})
4 tpidm23 4324 . . . . . . . . 9 {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵}
54eqcomi 2660 . . . . . . . 8 {𝐴, 𝐵} = {𝐴, 𝐵, 𝐵}
65fneq2i 6024 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐵})
7 tpidm23 4324 . . . . . . . . 9 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩}
87eqcomi 2660 . . . . . . . 8 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩}
98eqeq2i 2663 . . . . . . 7 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩})
103, 6, 93bitr3i 290 . . . . . 6 (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩})
1110a1i 11 . . . . 5 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩}))
12 tpeq3 4311 . . . . . 6 (𝐵 = 𝐶 → {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵, 𝐶})
1312fneq2d 6020 . . . . 5 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
14 id 22 . . . . . . . 8 (𝐵 = 𝐶𝐵 = 𝐶)
15 fveq2 6229 . . . . . . . 8 (𝐵 = 𝐶 → (𝐹𝐵) = (𝐹𝐶))
1614, 15opeq12d 4441 . . . . . . 7 (𝐵 = 𝐶 → ⟨𝐵, (𝐹𝐵)⟩ = ⟨𝐶, (𝐹𝐶)⟩)
1716tpeq3d 4314 . . . . . 6 (𝐵 = 𝐶 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
1817eqeq2d 2661 . . . . 5 (𝐵 = 𝐶 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
1911, 13, 183bitr3d 298 . . . 4 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
2019a1d 25 . . 3 (𝐵 = 𝐶 → ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})))
21 fndm 6028 . . . . . . . 8 (𝐹 Fn {𝐴, 𝐵, 𝐶} → dom 𝐹 = {𝐴, 𝐵, 𝐶})
22 fvex 6239 . . . . . . . . 9 (𝐹𝐴) ∈ V
23 fvex 6239 . . . . . . . . 9 (𝐹𝐵) ∈ V
24 fvex 6239 . . . . . . . . 9 (𝐹𝐶) ∈ V
2522, 23, 24dmtpop 5647 . . . . . . . 8 dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {𝐴, 𝐵, 𝐶}
2621, 25syl6eqr 2703 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵, 𝐶} → dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
2726adantl 481 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
2821adantl 481 . . . . . . . . 9 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → dom 𝐹 = {𝐴, 𝐵, 𝐶})
2928eleq2d 2716 . . . . . . . 8 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ dom 𝐹𝑥 ∈ {𝐴, 𝐵, 𝐶}))
30 vex 3234 . . . . . . . . . 10 𝑥 ∈ V
3130eltp 4262 . . . . . . . . 9 (𝑥 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶))
321, 22fvtp1 6501 . . . . . . . . . . . . 13 ((𝐴𝐵𝐴𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴) = (𝐹𝐴))
3332ad2antrr 762 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴) = (𝐹𝐴))
3433eqcomd 2657 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐴) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴))
35 fveq2 6229 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
36 fveq2 6229 . . . . . . . . . . . 12 (𝑥 = 𝐴 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴))
3735, 36eqeq12d 2666 . . . . . . . . . . 11 (𝑥 = 𝐴 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐴) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴)))
3834, 37syl5ibrcom 237 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐴 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
392, 23fvtp2 6502 . . . . . . . . . . . . 13 ((𝐴𝐵𝐵𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵) = (𝐹𝐵))
4039ad4ant13 1315 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵) = (𝐹𝐵))
4140eqcomd 2657 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐵) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵))
42 fveq2 6229 . . . . . . . . . . . 12 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
43 fveq2 6229 . . . . . . . . . . . 12 (𝑥 = 𝐵 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵))
4442, 43eqeq12d 2666 . . . . . . . . . . 11 (𝑥 = 𝐵 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐵) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵)))
4541, 44syl5ibrcom 237 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐵 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
46 fntpb.c . . . . . . . . . . . . . 14 𝐶 ∈ V
4746, 24fvtp3 6503 . . . . . . . . . . . . 13 ((𝐴𝐶𝐵𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶) = (𝐹𝐶))
4847ad4ant23 1325 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶) = (𝐹𝐶))
4948eqcomd 2657 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐶) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶))
50 fveq2 6229 . . . . . . . . . . . 12 (𝑥 = 𝐶 → (𝐹𝑥) = (𝐹𝐶))
51 fveq2 6229 . . . . . . . . . . . 12 (𝑥 = 𝐶 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶))
5250, 51eqeq12d 2666 . . . . . . . . . . 11 (𝑥 = 𝐶 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐶) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶)))
5349, 52syl5ibrcom 237 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐶 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5438, 45, 533jaod 1432 . . . . . . . . 9 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5531, 54syl5bi 232 . . . . . . . 8 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5629, 55sylbid 230 . . . . . . 7 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ dom 𝐹 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5756ralrimiv 2994 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))
58 fnfun 6026 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵, 𝐶} → Fun 𝐹)
591, 2, 46, 22, 23, 24funtp 5983 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
60593expa 1284 . . . . . . 7 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
61 eqfunfv 6356 . . . . . . 7 ((Fun 𝐹 ∧ Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}) → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))))
6258, 60, 61syl2anr 494 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))))
6327, 57, 62mpbir2and 977 . . . . 5 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
641, 2, 46, 22, 23, 24fntp 5987 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶})
65643expa 1284 . . . . . 6 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶})
66 fneq1 6017 . . . . . . 7 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶}))
6766biimprd 238 . . . . . 6 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶} → 𝐹 Fn {𝐴, 𝐵, 𝐶}))
6865, 67mpan9 485 . . . . 5 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}) → 𝐹 Fn {𝐴, 𝐵, 𝐶})
6963, 68impbida 895 . . . 4 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
7069expcom 450 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})))
7120, 70pm2.61ine 2906 . 2 ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
721, 46fnprb 6513 . . . . 5 (𝐹 Fn {𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
73 tpidm12 4322 . . . . . . 7 {𝐴, 𝐴, 𝐶} = {𝐴, 𝐶}
7473eqcomi 2660 . . . . . 6 {𝐴, 𝐶} = {𝐴, 𝐴, 𝐶}
7574fneq2i 6024 . . . . 5 (𝐹 Fn {𝐴, 𝐶} ↔ 𝐹 Fn {𝐴, 𝐴, 𝐶})
76 tpidm12 4322 . . . . . . 7 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}
7776eqcomi 2660 . . . . . 6 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}
7877eqeq2i 2663 . . . . 5 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
7972, 75, 783bitr3i 290 . . . 4 (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
8079a1i 11 . . 3 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
81 tpeq2 4310 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐴, 𝐶} = {𝐴, 𝐵, 𝐶})
8281fneq2d 6020 . . 3 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
83 id 22 . . . . . 6 (𝐴 = 𝐵𝐴 = 𝐵)
84 fveq2 6229 . . . . . 6 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
8583, 84opeq12d 4441 . . . . 5 (𝐴 = 𝐵 → ⟨𝐴, (𝐹𝐴)⟩ = ⟨𝐵, (𝐹𝐵)⟩)
8685tpeq2d 4313 . . . 4 (𝐴 = 𝐵 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
8786eqeq2d 2661 . . 3 (𝐴 = 𝐵 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
8880, 82, 873bitr3d 298 . 2 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
89 tpidm13 4323 . . . . . . 7 {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵}
9089eqcomi 2660 . . . . . 6 {𝐴, 𝐵} = {𝐴, 𝐵, 𝐴}
9190fneq2i 6024 . . . . 5 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐴})
92 tpidm13 4323 . . . . . . 7 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩}
9392eqcomi 2660 . . . . . 6 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩}
9493eqeq2i 2663 . . . . 5 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩})
953, 91, 943bitr3i 290 . . . 4 (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩})
9695a1i 11 . . 3 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩}))
97 tpeq3 4311 . . . 4 (𝐴 = 𝐶 → {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵, 𝐶})
9897fneq2d 6020 . . 3 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
99 id 22 . . . . . 6 (𝐴 = 𝐶𝐴 = 𝐶)
100 fveq2 6229 . . . . . 6 (𝐴 = 𝐶 → (𝐹𝐴) = (𝐹𝐶))
10199, 100opeq12d 4441 . . . . 5 (𝐴 = 𝐶 → ⟨𝐴, (𝐹𝐴)⟩ = ⟨𝐶, (𝐹𝐶)⟩)
102101tpeq3d 4314 . . . 4 (𝐴 = 𝐶 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
103102eqeq2d 2661 . . 3 (𝐴 = 𝐶 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
10496, 98, 1033bitr3d 298 . 2 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
10571, 88, 104pm2.61iine 2913 1 (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3o 1053   = wceq 1523  wcel 2030  wne 2823  wral 2941  Vcvv 3231  {cpr 4212  {ctp 4214  cop 4216  dom cdm 5143  Fun wfun 5920   Fn wfn 5921  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934
This theorem is referenced by:  wrd3tpop  13737
  Copyright terms: Public domain W3C validator