Proof of Theorem fprb
Step | Hyp | Ref
| Expression |
1 | | fprb.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
2 | 1 | prid1 4241 |
. . . . . 6
⊢ 𝐴 ∈ {𝐴, 𝐵} |
3 | | ffvelrn 6265 |
. . . . . 6
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ∈ {𝐴, 𝐵}) → (𝐹‘𝐴) ∈ 𝑅) |
4 | 2, 3 | mpan2 703 |
. . . . 5
⊢ (𝐹:{𝐴, 𝐵}⟶𝑅 → (𝐹‘𝐴) ∈ 𝑅) |
5 | 4 | adantr 480 |
. . . 4
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → (𝐹‘𝐴) ∈ 𝑅) |
6 | | fprb.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
7 | 6 | prid2 4242 |
. . . . . 6
⊢ 𝐵 ∈ {𝐴, 𝐵} |
8 | | ffvelrn 6265 |
. . . . . 6
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐵 ∈ {𝐴, 𝐵}) → (𝐹‘𝐵) ∈ 𝑅) |
9 | 7, 8 | mpan2 703 |
. . . . 5
⊢ (𝐹:{𝐴, 𝐵}⟶𝑅 → (𝐹‘𝐵) ∈ 𝑅) |
10 | 9 | adantr 480 |
. . . 4
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → (𝐹‘𝐵) ∈ 𝑅) |
11 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐹‘𝐴) ∈ V |
12 | 1, 11 | fvpr1 6361 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴)) |
13 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐹‘𝐵) ∈ V |
14 | 6, 13 | fvpr2 6362 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵)) |
15 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
16 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴)) |
17 | 15, 16 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴))) |
18 | | eqcom 2617 |
. . . . . . . . 9
⊢ ((𝐹‘𝐴) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) ↔ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴)) |
19 | 17, 18 | syl6bb 275 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴))) |
20 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
21 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵)) |
22 | 20, 21 | eqeq12d 2625 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵))) |
23 | | eqcom 2617 |
. . . . . . . . 9
⊢ ((𝐹‘𝐵) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) ↔ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵)) |
24 | 22, 23 | syl6bb 275 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵))) |
25 | 1, 6, 19, 24 | ralpr 4185 |
. . . . . . 7
⊢
(∀𝑥 ∈
{𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥) ↔ (({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐴) = (𝐹‘𝐴) ∧ ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝐵) = (𝐹‘𝐵))) |
26 | 12, 14, 25 | sylanbrc 695 |
. . . . . 6
⊢ (𝐴 ≠ 𝐵 → ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)) |
27 | 26 | adantl 481 |
. . . . 5
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥)) |
28 | | ffn 5958 |
. . . . . 6
⊢ (𝐹:{𝐴, 𝐵}⟶𝑅 → 𝐹 Fn {𝐴, 𝐵}) |
29 | 1, 6, 11, 13 | fpr 6326 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}:{𝐴, 𝐵}⟶{(𝐹‘𝐴), (𝐹‘𝐵)}) |
30 | | ffn 5958 |
. . . . . . 7
⊢
({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}:{𝐴, 𝐵}⟶{(𝐹‘𝐴), (𝐹‘𝐵)} → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵}) |
31 | 29, 30 | syl 17 |
. . . . . 6
⊢ (𝐴 ≠ 𝐵 → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵}) |
32 | | eqfnfv 6219 |
. . . . . 6
⊢ ((𝐹 Fn {𝐴, 𝐵} ∧ {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} Fn {𝐴, 𝐵}) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
33 | 28, 31, 32 | syl2an 493 |
. . . . 5
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉} ↔ ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}‘𝑥))) |
34 | 27, 33 | mpbird 246 |
. . . 4
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
35 | | opeq2 4341 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝐴) → 〈𝐴, 𝑥〉 = 〈𝐴, (𝐹‘𝐴)〉) |
36 | 35 | preq1d 4218 |
. . . . . 6
⊢ (𝑥 = (𝐹‘𝐴) → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, 𝑦〉}) |
37 | 36 | eqeq2d 2620 |
. . . . 5
⊢ (𝑥 = (𝐹‘𝐴) → (𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, 𝑦〉})) |
38 | | opeq2 4341 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝐵) → 〈𝐵, 𝑦〉 = 〈𝐵, (𝐹‘𝐵)〉) |
39 | 38 | preq2d 4219 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝐵) → {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, 𝑦〉} = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) |
40 | 39 | eqeq2d 2620 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝐵) → (𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, 𝑦〉} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉})) |
41 | 37, 40 | rspc2ev 3295 |
. . . 4
⊢ (((𝐹‘𝐴) ∈ 𝑅 ∧ (𝐹‘𝐵) ∈ 𝑅 ∧ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉, 〈𝐵, (𝐹‘𝐵)〉}) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}) |
42 | 5, 10, 34, 41 | syl3anc 1318 |
. . 3
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}) |
43 | 42 | expcom 450 |
. 2
⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉})) |
44 | | vex 3176 |
. . . . . . 7
⊢ 𝑥 ∈ V |
45 | | vex 3176 |
. . . . . . 7
⊢ 𝑦 ∈ V |
46 | 1, 6, 44, 45 | fpr 6326 |
. . . . . 6
⊢ (𝐴 ≠ 𝐵 → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶{𝑥, 𝑦}) |
47 | | prssi 4293 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → {𝑥, 𝑦} ⊆ 𝑅) |
48 | | fss 5969 |
. . . . . 6
⊢
(({〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶{𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝑅) → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅) |
49 | 46, 47, 48 | syl2an 493 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅) |
50 | 49 | ex 449 |
. . . 4
⊢ (𝐴 ≠ 𝐵 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅)) |
51 | | feq1 5939 |
. . . . 5
⊢ (𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅)) |
52 | 51 | biimprcd 239 |
. . . 4
⊢
({〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉}:{𝐴, 𝐵}⟶𝑅 → (𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} → 𝐹:{𝐴, 𝐵}⟶𝑅)) |
53 | 50, 52 | syl6 34 |
. . 3
⊢ (𝐴 ≠ 𝐵 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} → 𝐹:{𝐴, 𝐵}⟶𝑅))) |
54 | 53 | rexlimdvv 3019 |
. 2
⊢ (𝐴 ≠ 𝐵 → (∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉} → 𝐹:{𝐴, 𝐵}⟶𝑅)) |
55 | 43, 54 | impbid 201 |
1
⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉})) |