Proof of Theorem fprb
Step | Hyp | Ref
| Expression |
1 | | fprb.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
2 | 1 | prid1 4678 |
. . . . . 6
⊢ 𝐴 ∈ {𝐴, 𝐵} |
3 | | ffvelrn 6902 |
. . . . . 6
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ∈ {𝐴, 𝐵}) → (𝐹‘𝐴) ∈ 𝑅) |
4 | 2, 3 | mpan2 691 |
. . . . 5
⊢ (𝐹:{𝐴, 𝐵}⟶𝑅 → (𝐹‘𝐴) ∈ 𝑅) |
5 | 4 | adantr 484 |
. . . 4
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → (𝐹‘𝐴) ∈ 𝑅) |
6 | | fprb.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
7 | 6 | prid2 4679 |
. . . . . 6
⊢ 𝐵 ∈ {𝐴, 𝐵} |
8 | | ffvelrn 6902 |
. . . . . 6
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐵 ∈ {𝐴, 𝐵}) → (𝐹‘𝐵) ∈ 𝑅) |
9 | 7, 8 | mpan2 691 |
. . . . 5
⊢ (𝐹:{𝐴, 𝐵}⟶𝑅 → (𝐹‘𝐵) ∈ 𝑅) |
10 | 9 | adantr 484 |
. . . 4
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → (𝐹‘𝐵) ∈ 𝑅) |
11 | | fvex 6730 |
. . . . . . . 8
⊢ (𝐹‘𝐴) ∈ V |
12 | 1, 11 | fvpr1 7005 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴)) |
13 | | fvex 6730 |
. . . . . . . 8
⊢ (𝐹‘𝐵) ∈ V |
14 | 6, 13 | fvpr2 7006 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵)) |
15 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
16 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴)) |
17 | 15, 16 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴))) |
18 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) ↔ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴)) |
19 | 17, 18 | bitrdi 290 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴))) |
20 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
21 | | fveq2 6717 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵)) |
22 | 20, 21 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵))) |
23 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) ↔ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵)) |
24 | 22, 23 | bitrdi 290 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵))) |
25 | 1, 6, 19, 24 | ralpr 4616 |
. . . . . . 7
⊢
(∀𝑥 ∈
{𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴) ∧ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵))) |
26 | 12, 14, 25 | sylanbrc 586 |
. . . . . 6
⊢ (𝐴 ≠ 𝐵 → ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)) |
27 | 26 | adantl 485 |
. . . . 5
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)) |
28 | | ffn 6545 |
. . . . . 6
⊢ (𝐹:{𝐴, 𝐵}⟶𝑅 → 𝐹 Fn {𝐴, 𝐵}) |
29 | 1, 6, 11, 13 | fpr 6969 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}:{𝐴, 𝐵}⟶{(𝐹‘𝐴), (𝐹‘𝐵)}) |
30 | 29 | ffnd 6546 |
. . . . . 6
⊢ (𝐴 ≠ 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵}) |
31 | | eqfnfv 6852 |
. . . . . 6
⊢ ((𝐹 Fn {𝐴, 𝐵} ∧ {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵}) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
32 | 28, 30, 31 | syl2an 599 |
. . . . 5
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
33 | 27, 32 | mpbird 260 |
. . . 4
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
34 | | opeq2 4785 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝐴) → 〈𝐴, 𝑥〉 = 〈𝐴, (𝐹‘𝐴)〉) |
35 | 34 | preq1d 4655 |
. . . . . 6
⊢ (𝑥 = (𝐹‘𝐴) → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, 𝑦〉}) |
36 | 35 | eqeq2d 2748 |
. . . . 5
⊢ (𝑥 = (𝐹‘𝐴) → (𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, 𝑦〉})) |
37 | | opeq2 4785 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝐵) → 〈𝐵, 𝑦〉 = 〈𝐵, (𝐹‘𝐵)〉) |
38 | 37 | preq2d 4656 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝐵) → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, 𝑦〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
39 | 38 | eqeq2d 2748 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝐵) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, 𝑦〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) |
40 | 36, 39 | rspc2ev 3549 |
. . . 4
⊢ (((𝐹‘𝐴) ∈ 𝑅 ∧ (𝐹‘𝐵) ∈ 𝑅 ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}) |
41 | 5, 10, 33, 40 | syl3anc 1373 |
. . 3
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}) |
42 | 41 | expcom 417 |
. 2
⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉})) |
43 | | vex 3412 |
. . . . . . 7
⊢ 𝑥 ∈ V |
44 | | vex 3412 |
. . . . . . 7
⊢ 𝑦 ∈ V |
45 | 1, 6, 43, 44 | fpr 6969 |
. . . . . 6
⊢ (𝐴 ≠ 𝐵 → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶{𝑥, 𝑦}) |
46 | | prssi 4734 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → {𝑥, 𝑦} ⊆ 𝑅) |
47 | | fss 6562 |
. . . . . 6
⊢
(({〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶{𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝑅) → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅) |
48 | 45, 46, 47 | syl2an 599 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅) |
49 | 48 | ex 416 |
. . . 4
⊢ (𝐴 ≠ 𝐵 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅)) |
50 | | feq1 6526 |
. . . . 5
⊢ (𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅)) |
51 | 50 | biimprcd 253 |
. . . 4
⊢
({〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅 → (𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} → 𝐹:{𝐴, 𝐵}⟶𝑅)) |
52 | 49, 51 | syl6 35 |
. . 3
⊢ (𝐴 ≠ 𝐵 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} → 𝐹:{𝐴, 𝐵}⟶𝑅))) |
53 | 52 | rexlimdvv 3212 |
. 2
⊢ (𝐴 ≠ 𝐵 → (∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} → 𝐹:{𝐴, 𝐵}⟶𝑅)) |
54 | 42, 53 | impbid 215 |
1
⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉})) |