| Step | Hyp | Ref
| Expression |
| 1 | | fnprb.a |
. . . . . . . 8
⊢ 𝐴 ∈ V |
| 2 | | fnprb.b |
. . . . . . . 8
⊢ 𝐵 ∈ V |
| 3 | 1, 2 | fnprb 7228 |
. . . . . . 7
⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
| 4 | | tpidm23 4757 |
. . . . . . . . 9
⊢ {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵} |
| 5 | 4 | eqcomi 2746 |
. . . . . . . 8
⊢ {𝐴, 𝐵} = {𝐴, 𝐵, 𝐵} |
| 6 | 5 | fneq2i 6666 |
. . . . . . 7
⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐵}) |
| 7 | | tpidm23 4757 |
. . . . . . . . 9
⊢
{〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐵, (𝐹‘𝐵)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} |
| 8 | 7 | eqcomi 2746 |
. . . . . . . 8
⊢
{〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐵, (𝐹‘𝐵)〉} |
| 9 | 8 | eqeq2i 2750 |
. . . . . . 7
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
| 10 | 3, 6, 9 | 3bitr3i 301 |
. . . . . 6
⊢ (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
| 11 | 10 | a1i 11 |
. . . . 5
⊢ (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐵, (𝐹‘𝐵)〉})) |
| 12 | | tpeq3 4744 |
. . . . . 6
⊢ (𝐵 = 𝐶 → {𝐴, 𝐵, 𝐵} = {𝐴, 𝐵, 𝐶}) |
| 13 | 12 | fneq2d 6662 |
. . . . 5
⊢ (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶})) |
| 14 | | id 22 |
. . . . . . . 8
⊢ (𝐵 = 𝐶 → 𝐵 = 𝐶) |
| 15 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝐵 = 𝐶 → (𝐹‘𝐵) = (𝐹‘𝐶)) |
| 16 | 14, 15 | opeq12d 4881 |
. . . . . . 7
⊢ (𝐵 = 𝐶 → 〈𝐵, (𝐹‘𝐵)〉 = 〈𝐶, (𝐹‘𝐶)〉) |
| 17 | 16 | tpeq3d 4747 |
. . . . . 6
⊢ (𝐵 = 𝐶 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐵, (𝐹‘𝐵)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}) |
| 18 | 17 | eqeq2d 2748 |
. . . . 5
⊢ (𝐵 = 𝐶 → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉})) |
| 19 | 11, 13, 18 | 3bitr3d 309 |
. . . 4
⊢ (𝐵 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉})) |
| 20 | 19 | a1d 25 |
. . 3
⊢ (𝐵 = 𝐶 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}))) |
| 21 | | fndm 6671 |
. . . . . . . 8
⊢ (𝐹 Fn {𝐴, 𝐵, 𝐶} → dom 𝐹 = {𝐴, 𝐵, 𝐶}) |
| 22 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝐹‘𝐴) ∈ V |
| 23 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝐹‘𝐵) ∈ V |
| 24 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝐹‘𝐶) ∈ V |
| 25 | 22, 23, 24 | dmtpop 6238 |
. . . . . . . 8
⊢ dom
{〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉} = {𝐴, 𝐵, 𝐶} |
| 26 | 21, 25 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝐹 Fn {𝐴, 𝐵, 𝐶} → dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}) |
| 27 | 26 | adantl 481 |
. . . . . 6
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}) |
| 28 | 21 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → dom 𝐹 = {𝐴, 𝐵, 𝐶}) |
| 29 | 28 | eleq2d 2827 |
. . . . . . . 8
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ {𝐴, 𝐵, 𝐶})) |
| 30 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 31 | 30 | eltp 4689 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝐴, 𝐵, 𝐶} ↔ (𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶)) |
| 32 | 1, 22 | fvtp1 7215 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐴) = (𝐹‘𝐴)) |
| 33 | 32 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐴) = (𝐹‘𝐴)) |
| 34 | 33 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐴)) |
| 35 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
| 36 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐴)) |
| 37 | 35, 36 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥) ↔ (𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐴))) |
| 38 | 34, 37 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐴 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥))) |
| 39 | 2, 23 | fvtp2 7216 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐵) = (𝐹‘𝐵)) |
| 40 | 39 | ad4ant13 751 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐵) = (𝐹‘𝐵)) |
| 41 | 40 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐵)) |
| 42 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
| 43 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐵)) |
| 44 | 42, 43 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥) ↔ (𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐵))) |
| 45 | 41, 44 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐵 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥))) |
| 46 | | fntpb.c |
. . . . . . . . . . . . . 14
⊢ 𝐶 ∈ V |
| 47 | 46, 24 | fvtp3 7217 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐶) = (𝐹‘𝐶)) |
| 48 | 47 | ad4ant23 753 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐶) = (𝐹‘𝐶)) |
| 49 | 48 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹‘𝐶) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐶)) |
| 50 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶)) |
| 51 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐶 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐶)) |
| 52 | 50, 51 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥) ↔ (𝐹‘𝐶) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝐶))) |
| 53 | 49, 52 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 = 𝐶 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥))) |
| 54 | 38, 45, 53 | 3jaod 1431 |
. . . . . . . . 9
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ((𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ∨ 𝑥 = 𝐶) → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥))) |
| 55 | 31, 54 | biimtrid 242 |
. . . . . . . 8
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥))) |
| 56 | 29, 55 | sylbid 240 |
. . . . . . 7
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝑥 ∈ dom 𝐹 → (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥))) |
| 57 | 56 | ralrimiv 3145 |
. . . . . 6
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥)) |
| 58 | | fnfun 6668 |
. . . . . . 7
⊢ (𝐹 Fn {𝐴, 𝐵, 𝐶} → Fun 𝐹) |
| 59 | 1, 2, 46, 22, 23, 24 | funtp 6623 |
. . . . . . . 8
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → Fun {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}) |
| 60 | 59 | 3expa 1119 |
. . . . . . 7
⊢ (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) → Fun {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}) |
| 61 | | eqfunfv 7056 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ Fun {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉} ↔ (dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉} ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥)))) |
| 62 | 58, 60, 61 | syl2anr 597 |
. . . . . 6
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉} ↔ (dom 𝐹 = dom {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉} ∧ ∀𝑥 ∈ dom 𝐹(𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}‘𝑥)))) |
| 63 | 27, 57, 62 | mpbir2and 713 |
. . . . 5
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 Fn {𝐴, 𝐵, 𝐶}) → 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}) |
| 64 | 1, 2, 46, 22, 23, 24 | fntp 6627 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉} Fn {𝐴, 𝐵, 𝐶}) |
| 65 | 64 | 3expa 1119 |
. . . . . 6
⊢ (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉} Fn {𝐴, 𝐵, 𝐶}) |
| 66 | | fneq1 6659 |
. . . . . . 7
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉} → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉} Fn {𝐴, 𝐵, 𝐶})) |
| 67 | 66 | biimprd 248 |
. . . . . 6
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉} → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉} Fn {𝐴, 𝐵, 𝐶} → 𝐹 Fn {𝐴, 𝐵, 𝐶})) |
| 68 | 65, 67 | mpan9 506 |
. . . . 5
⊢ ((((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}) → 𝐹 Fn {𝐴, 𝐵, 𝐶}) |
| 69 | 63, 68 | impbida 801 |
. . . 4
⊢ (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ 𝐵 ≠ 𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉})) |
| 70 | 69 | expcom 413 |
. . 3
⊢ (𝐵 ≠ 𝐶 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}))) |
| 71 | 20, 70 | pm2.61ine 3025 |
. 2
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉})) |
| 72 | 1, 46 | fnprb 7228 |
. . . . 5
⊢ (𝐹 Fn {𝐴, 𝐶} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐶, (𝐹‘𝐶)〉}) |
| 73 | | tpidm12 4755 |
. . . . . . 7
⊢ {𝐴, 𝐴, 𝐶} = {𝐴, 𝐶} |
| 74 | 73 | eqcomi 2746 |
. . . . . 6
⊢ {𝐴, 𝐶} = {𝐴, 𝐴, 𝐶} |
| 75 | 74 | fneq2i 6666 |
. . . . 5
⊢ (𝐹 Fn {𝐴, 𝐶} ↔ 𝐹 Fn {𝐴, 𝐴, 𝐶}) |
| 76 | | tpidm12 4755 |
. . . . . . 7
⊢
{〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉, 〈𝐶, (𝐹‘𝐶)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐶, (𝐹‘𝐶)〉} |
| 77 | 76 | eqcomi 2746 |
. . . . . 6
⊢
{〈𝐴, (𝐹‘𝐴)〉, 〈𝐶, (𝐹‘𝐶)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉, 〈𝐶, (𝐹‘𝐶)〉} |
| 78 | 77 | eqeq2i 2750 |
. . . . 5
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐶, (𝐹‘𝐶)〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉, 〈𝐶, (𝐹‘𝐶)〉}) |
| 79 | 72, 75, 78 | 3bitr3i 301 |
. . . 4
⊢ (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉, 〈𝐶, (𝐹‘𝐶)〉}) |
| 80 | 79 | a1i 11 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉, 〈𝐶, (𝐹‘𝐶)〉})) |
| 81 | | tpeq2 4743 |
. . . 4
⊢ (𝐴 = 𝐵 → {𝐴, 𝐴, 𝐶} = {𝐴, 𝐵, 𝐶}) |
| 82 | 81 | fneq2d 6662 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐴, 𝐶} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶})) |
| 83 | | id 22 |
. . . . . 6
⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) |
| 84 | | fveq2 6906 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐹‘𝐴) = (𝐹‘𝐵)) |
| 85 | 83, 84 | opeq12d 4881 |
. . . . 5
⊢ (𝐴 = 𝐵 → 〈𝐴, (𝐹‘𝐴)〉 = 〈𝐵, (𝐹‘𝐵)〉) |
| 86 | 85 | tpeq2d 4746 |
. . . 4
⊢ (𝐴 = 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉, 〈𝐶, (𝐹‘𝐶)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}) |
| 87 | 86 | eqeq2d 2748 |
. . 3
⊢ (𝐴 = 𝐵 → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐴, (𝐹‘𝐴)〉, 〈𝐶, (𝐹‘𝐶)〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉})) |
| 88 | 80, 82, 87 | 3bitr3d 309 |
. 2
⊢ (𝐴 = 𝐵 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉})) |
| 89 | | tpidm13 4756 |
. . . . . . 7
⊢ {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵} |
| 90 | 89 | eqcomi 2746 |
. . . . . 6
⊢ {𝐴, 𝐵} = {𝐴, 𝐵, 𝐴} |
| 91 | 90 | fneq2i 6666 |
. . . . 5
⊢ (𝐹 Fn {𝐴, 𝐵} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐴}) |
| 92 | | tpidm13 4756 |
. . . . . . 7
⊢
{〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐴, (𝐹‘𝐴)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} |
| 93 | 92 | eqcomi 2746 |
. . . . . 6
⊢
{〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐴, (𝐹‘𝐴)〉} |
| 94 | 93 | eqeq2i 2750 |
. . . . 5
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐴, (𝐹‘𝐴)〉}) |
| 95 | 3, 91, 94 | 3bitr3i 301 |
. . . 4
⊢ (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐴, (𝐹‘𝐴)〉}) |
| 96 | 95 | a1i 11 |
. . 3
⊢ (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐴, (𝐹‘𝐴)〉})) |
| 97 | | tpeq3 4744 |
. . . 4
⊢ (𝐴 = 𝐶 → {𝐴, 𝐵, 𝐴} = {𝐴, 𝐵, 𝐶}) |
| 98 | 97 | fneq2d 6662 |
. . 3
⊢ (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐴} ↔ 𝐹 Fn {𝐴, 𝐵, 𝐶})) |
| 99 | | id 22 |
. . . . . 6
⊢ (𝐴 = 𝐶 → 𝐴 = 𝐶) |
| 100 | | fveq2 6906 |
. . . . . 6
⊢ (𝐴 = 𝐶 → (𝐹‘𝐴) = (𝐹‘𝐶)) |
| 101 | 99, 100 | opeq12d 4881 |
. . . . 5
⊢ (𝐴 = 𝐶 → 〈𝐴, (𝐹‘𝐴)〉 = 〈𝐶, (𝐹‘𝐶)〉) |
| 102 | 101 | tpeq3d 4747 |
. . . 4
⊢ (𝐴 = 𝐶 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐴, (𝐹‘𝐴)〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}) |
| 103 | 102 | eqeq2d 2748 |
. . 3
⊢ (𝐴 = 𝐶 → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐴, (𝐹‘𝐴)〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉})) |
| 104 | 96, 98, 103 | 3bitr3d 309 |
. 2
⊢ (𝐴 = 𝐶 → (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉})) |
| 105 | 71, 88, 104 | pm2.61iine 3032 |
1
⊢ (𝐹 Fn {𝐴, 𝐵, 𝐶} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉, 〈𝐶, (𝐹‘𝐶)〉}) |