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

Theorem fntpb 6356
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 6355 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩})
4 tpidm23 4235 . . . . . . . . 9 {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵}
54eqcomi 2618 . . . . . . . 8 {𝐴, 𝐵} = {𝐴, 𝐵, 𝐵}
65fneq2i 5886 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐵})
7 tpidm23 4235 . . . . . . . . 9 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩}
87eqcomi 2618 . . . . . . . 8 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩}
98eqeq2i 2621 . . . . . . 7 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩})
103, 6, 93bitr3i 288 . . . . . 6 (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩})
1110a1i 11 . . . . 5 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩}))
12 tpeq3 4222 . . . . . 6 (𝐵 = 𝐶 → {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵, 𝐶})
1312fneq2d 5882 . . . . 5 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
14 id 22 . . . . . . . 8 (𝐵 = 𝐶𝐵 = 𝐶)
15 fveq2 6088 . . . . . . . 8 (𝐵 = 𝐶 → (𝐹𝐵) = (𝐹𝐶))
1614, 15opeq12d 4342 . . . . . . 7 (𝐵 = 𝐶 → ⟨𝐵, (𝐹𝐵)⟩ = ⟨𝐶, (𝐹𝐶)⟩)
1716tpeq3d 4225 . . . . . 6 (𝐵 = 𝐶 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
1817eqeq2d 2619 . . . . 5 (𝐵 = 𝐶 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
1911, 13, 183bitr3d 296 . . . 4 (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
2019a1d 25 . . 3 (𝐵 = 𝐶 → ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})))
21 fndm 5890 . . . . . . . 8 (𝐹 Fn {𝐴, 𝐵, 𝐶} → dom 𝐹 = {𝐴, 𝐵, 𝐶})
22 fvex 6098 . . . . . . . . 9 (𝐹𝐴) ∈ V
23 fvex 6098 . . . . . . . . 9 (𝐹𝐵) ∈ V
24 fvex 6098 . . . . . . . . 9 (𝐹𝐶) ∈ V
2522, 23, 24dmtpop 5515 . . . . . . . 8 dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {𝐴, 𝐵, 𝐶}
2621, 25syl6eqr 2661 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵, 𝐶} → dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
2726adantl 480 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
2821adantl 480 . . . . . . . . 9 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → dom 𝐹 = {𝐴, 𝐵, 𝐶})
2928eleq2d 2672 . . . . . . . 8 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ dom 𝐹𝑥 ∈ {𝐴, 𝐵, 𝐶}))
30 vex 3175 . . . . . . . . . 10 𝑥 ∈ V
3130eltp 4176 . . . . . . . . 9 (𝑥 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶))
321, 22fvtp1 6343 . . . . . . . . . . . . 13 ((𝐴𝐵𝐴𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴) = (𝐹𝐴))
3332ad2antrr 757 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴) = (𝐹𝐴))
3433eqcomd 2615 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐴) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴))
35 fveq2 6088 . . . . . . . . . . . 12 (𝑥 = 𝐴 → (𝐹𝑥) = (𝐹𝐴))
36 fveq2 6088 . . . . . . . . . . . 12 (𝑥 = 𝐴 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴))
3735, 36eqeq12d 2624 . . . . . . . . . . 11 (𝑥 = 𝐴 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐴) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐴)))
3834, 37syl5ibrcom 235 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐴 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
392, 23fvtp2 6344 . . . . . . . . . . . . 13 ((𝐴𝐵𝐵𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵) = (𝐹𝐵))
4039ad4ant13 1283 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵) = (𝐹𝐵))
4140eqcomd 2615 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐵) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵))
42 fveq2 6088 . . . . . . . . . . . 12 (𝑥 = 𝐵 → (𝐹𝑥) = (𝐹𝐵))
43 fveq2 6088 . . . . . . . . . . . 12 (𝑥 = 𝐵 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵))
4442, 43eqeq12d 2624 . . . . . . . . . . 11 (𝑥 = 𝐵 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐵) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐵)))
4541, 44syl5ibrcom 235 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐵 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
46 fntpb.c . . . . . . . . . . . . . 14 𝐶 ∈ V
4746, 24fvtp3 6345 . . . . . . . . . . . . 13 ((𝐴𝐶𝐵𝐶) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶) = (𝐹𝐶))
4847ad4ant23 1288 . . . . . . . . . . . 12 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶) = (𝐹𝐶))
4948eqcomd 2615 . . . . . . . . . . 11 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹𝐶) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶))
50 fveq2 6088 . . . . . . . . . . . 12 (𝑥 = 𝐶 → (𝐹𝑥) = (𝐹𝐶))
51 fveq2 6088 . . . . . . . . . . . 12 (𝑥 = 𝐶 → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶))
5250, 51eqeq12d 2624 . . . . . . . . . . 11 (𝑥 = 𝐶 → ((𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥) ↔ (𝐹𝐶) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝐶)))
5349, 52syl5ibrcom 235 . . . . . . . . . 10 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐶 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5438, 45, 533jaod 1383 . . . . . . . . 9 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ((𝑥 = 𝐴𝑥 = 𝐵𝑥 = 𝐶) → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5531, 54syl5bi 230 . . . . . . . 8 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5629, 55sylbid 228 . . . . . . 7 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ dom 𝐹 → (𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥)))
5756ralrimiv 2947 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))
58 fnfun 5888 . . . . . . 7 (𝐹 Fn {𝐴, 𝐵, 𝐶} → Fun 𝐹)
591, 2, 46, 22, 23, 24funtp 5845 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
60593expa 1256 . . . . . . 7 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
61 eqfunfv 6209 . . . . . . 7 ((Fun 𝐹 ∧ Fun {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}) → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))))
6258, 60, 61syl2anr 493 . . . . . 6 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ (dom 𝐹 = dom {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} ∧ ∀𝑥 ∈ dom 𝐹(𝐹𝑥) = ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}‘𝑥))))
6327, 57, 62mpbir2and 958 . . . . 5 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
641, 2, 46, 22, 23, 24fntp 5849 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶})
65643expa 1256 . . . . . 6 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶})
66 fneq1 5879 . . . . . . 7 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶}))
6766biimprd 236 . . . . . 6 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} → ({⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩} Fn {𝐴, 𝐵, 𝐶} → 𝐹 Fn {𝐴, 𝐵, 𝐶}))
6865, 67mpan9 484 . . . . 5 ((((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) ∧ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}) → 𝐹 Fn {𝐴, 𝐵, 𝐶})
6963, 68impbida 872 . . . 4 (((𝐴𝐵𝐴𝐶) ∧ 𝐵𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
7069expcom 449 . . 3 (𝐵𝐶 → ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})))
7120, 70pm2.61ine 2864 . 2 ((𝐴𝐵𝐴𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
721, 46fnprb 6355 . . . . 5 (𝐹 Fn {𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
73 tpidm12 4233 . . . . . . 7 {𝐴, 𝐴, 𝐶} = {𝐴, 𝐶}
7473eqcomi 2618 . . . . . 6 {𝐴, 𝐶} = {𝐴, 𝐴, 𝐶}
7574fneq2i 5886 . . . . 5 (𝐹 Fn {𝐴, 𝐶} ↔ 𝐹 Fn {𝐴, 𝐴, 𝐶})
76 tpidm12 4233 . . . . . . 7 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}
7776eqcomi 2618 . . . . . 6 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}
7877eqeq2i 2621 . . . . 5 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
7972, 75, 783bitr3i 288 . . . 4 (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩})
8079a1i 11 . . 3 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
81 tpeq2 4221 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐴, 𝐶} = {𝐴, 𝐵, 𝐶})
8281fneq2d 5882 . . 3 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
83 id 22 . . . . . 6 (𝐴 = 𝐵𝐴 = 𝐵)
84 fveq2 6088 . . . . . 6 (𝐴 = 𝐵 → (𝐹𝐴) = (𝐹𝐵))
8583, 84opeq12d 4342 . . . . 5 (𝐴 = 𝐵 → ⟨𝐴, (𝐹𝐴)⟩ = ⟨𝐵, (𝐹𝐵)⟩)
8685tpeq2d 4224 . . . 4 (𝐴 = 𝐵 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
8786eqeq2d 2619 . . 3 (𝐴 = 𝐵 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐴, (𝐹𝐴)⟩, ⟨𝐶, (𝐹𝐶)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
8880, 82, 873bitr3d 296 . 2 (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
89 tpidm13 4234 . . . . . . 7 {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵}
9089eqcomi 2618 . . . . . 6 {𝐴, 𝐵} = {𝐴, 𝐵, 𝐴}
9190fneq2i 5886 . . . . 5 (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐴})
92 tpidm13 4234 . . . . . . 7 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩}
9392eqcomi 2618 . . . . . 6 {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩}
9493eqeq2i 2621 . . . . 5 (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩})
953, 91, 943bitr3i 288 . . . 4 (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩})
9695a1i 11 . . 3 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩}))
97 tpeq3 4222 . . . 4 (𝐴 = 𝐶 → {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵, 𝐶})
9897fneq2d 5882 . . 3 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶}))
99 id 22 . . . . . 6 (𝐴 = 𝐶𝐴 = 𝐶)
100 fveq2 6088 . . . . . 6 (𝐴 = 𝐶 → (𝐹𝐴) = (𝐹𝐶))
10199, 100opeq12d 4342 . . . . 5 (𝐴 = 𝐶 → ⟨𝐴, (𝐹𝐴)⟩ = ⟨𝐶, (𝐹𝐶)⟩)
102101tpeq3d 4225 . . . 4 (𝐴 = 𝐶 → {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
103102eqeq2d 2619 . . 3 (𝐴 = 𝐶 → (𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐴, (𝐹𝐴)⟩} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
10496, 98, 1033bitr3d 296 . 2 (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩}))
10571, 88, 104pm2.61iine 2871 1 (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {⟨𝐴, (𝐹𝐴)⟩, ⟨𝐵, (𝐹𝐵)⟩, ⟨𝐶, (𝐹𝐶)⟩})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3o 1029   = wceq 1474  wcel 1976  wne 2779  wral 2895  Vcvv 3172  {cpr 4126  {ctp 4128  cop 4130  dom cdm 5028  Fun wfun 5784   Fn wfn 5785  cfv 5790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798
This theorem is referenced by:  wrd3tpop  13485
  Copyright terms: Public domain W3C validator