Proof of Theorem fprb
| Step | Hyp | Ref
| Expression |
| 1 | | fprb.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
| 2 | 1 | prid1 4762 |
. . . . . 6
⊢ 𝐴 ∈ {𝐴, 𝐵} |
| 3 | | ffvelcdm 7101 |
. . . . . 6
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ∈ {𝐴, 𝐵}) → (𝐹‘𝐴) ∈ 𝑅) |
| 4 | 2, 3 | mpan2 691 |
. . . . 5
⊢ (𝐹:{𝐴, 𝐵}⟶𝑅 → (𝐹‘𝐴) ∈ 𝑅) |
| 5 | 4 | adantr 480 |
. . . 4
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → (𝐹‘𝐴) ∈ 𝑅) |
| 6 | | fprb.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
| 7 | 6 | prid2 4763 |
. . . . . 6
⊢ 𝐵 ∈ {𝐴, 𝐵} |
| 8 | | ffvelcdm 7101 |
. . . . . 6
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐵 ∈ {𝐴, 𝐵}) → (𝐹‘𝐵) ∈ 𝑅) |
| 9 | 7, 8 | mpan2 691 |
. . . . 5
⊢ (𝐹:{𝐴, 𝐵}⟶𝑅 → (𝐹‘𝐵) ∈ 𝑅) |
| 10 | 9 | adantr 480 |
. . . 4
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → (𝐹‘𝐵) ∈ 𝑅) |
| 11 | | fvex 6919 |
. . . . . . . 8
⊢ (𝐹‘𝐴) ∈ V |
| 12 | 1, 11 | fvpr1 7212 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴)) |
| 13 | | fvex 6919 |
. . . . . . . 8
⊢ (𝐹‘𝐵) ∈ V |
| 14 | 6, 13 | fvpr2 7213 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵)) |
| 15 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
| 16 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴)) |
| 17 | 15, 16 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴))) |
| 18 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) ↔ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴)) |
| 19 | 17, 18 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴))) |
| 20 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
| 21 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵)) |
| 22 | 20, 21 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵))) |
| 23 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) ↔ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵)) |
| 24 | 22, 23 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵))) |
| 25 | 1, 6, 19, 24 | ralpr 4700 |
. . . . . . 7
⊢
(∀𝑥 ∈
{𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴) ∧ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵))) |
| 26 | 12, 14, 25 | sylanbrc 583 |
. . . . . 6
⊢ (𝐴 ≠ 𝐵 → ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)) |
| 27 | 26 | adantl 481 |
. . . . 5
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)) |
| 28 | | ffn 6736 |
. . . . . 6
⊢ (𝐹:{𝐴, 𝐵}⟶𝑅 → 𝐹 Fn {𝐴, 𝐵}) |
| 29 | 1, 6, 11, 13 | fpr 7174 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}:{𝐴, 𝐵}⟶{(𝐹‘𝐴), (𝐹‘𝐵)}) |
| 30 | 29 | ffnd 6737 |
. . . . . 6
⊢ (𝐴 ≠ 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵}) |
| 31 | | eqfnfv 7051 |
. . . . . 6
⊢ ((𝐹 Fn {𝐴, 𝐵} ∧ {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵}) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
| 32 | 28, 30, 31 | syl2an 596 |
. . . . 5
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
| 33 | 27, 32 | mpbird 257 |
. . . 4
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
| 34 | | opeq2 4874 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝐴) → 〈𝐴, 𝑥〉 = 〈𝐴, (𝐹‘𝐴)〉) |
| 35 | 34 | preq1d 4739 |
. . . . . 6
⊢ (𝑥 = (𝐹‘𝐴) → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, 𝑦〉}) |
| 36 | 35 | eqeq2d 2748 |
. . . . 5
⊢ (𝑥 = (𝐹‘𝐴) → (𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, 𝑦〉})) |
| 37 | | opeq2 4874 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝐵) → 〈𝐵, 𝑦〉 = 〈𝐵, (𝐹‘𝐵)〉) |
| 38 | 37 | preq2d 4740 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝐵) → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, 𝑦〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
| 39 | 38 | eqeq2d 2748 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝐵) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, 𝑦〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) |
| 40 | 36, 39 | rspc2ev 3635 |
. . . 4
⊢ (((𝐹‘𝐴) ∈ 𝑅 ∧ (𝐹‘𝐵) ∈ 𝑅 ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}) |
| 41 | 5, 10, 33, 40 | syl3anc 1373 |
. . 3
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}) |
| 42 | 41 | expcom 413 |
. 2
⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉})) |
| 43 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 44 | | vex 3484 |
. . . . . . 7
⊢ 𝑦 ∈ V |
| 45 | 1, 6, 43, 44 | fpr 7174 |
. . . . . 6
⊢ (𝐴 ≠ 𝐵 → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶{𝑥, 𝑦}) |
| 46 | | prssi 4821 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → {𝑥, 𝑦} ⊆ 𝑅) |
| 47 | | fss 6752 |
. . . . . 6
⊢
(({〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶{𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝑅) → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅) |
| 48 | 45, 46, 47 | syl2an 596 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅) |
| 49 | 48 | ex 412 |
. . . 4
⊢ (𝐴 ≠ 𝐵 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅)) |
| 50 | | feq1 6716 |
. . . . 5
⊢ (𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅)) |
| 51 | 50 | biimprcd 250 |
. . . 4
⊢
({〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅 → (𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} → 𝐹:{𝐴, 𝐵}⟶𝑅)) |
| 52 | 49, 51 | syl6 35 |
. . 3
⊢ (𝐴 ≠ 𝐵 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} → 𝐹:{𝐴, 𝐵}⟶𝑅))) |
| 53 | 52 | rexlimdvv 3212 |
. 2
⊢ (𝐴 ≠ 𝐵 → (∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} → 𝐹:{𝐴, 𝐵}⟶𝑅)) |
| 54 | 42, 53 | impbid 212 |
1
⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉})) |