Step | Hyp | Ref
| Expression |
1 | | fprb.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
2 | 1 | prid1 4766 |
. . . . . 6
⊢ 𝐴 ∈ {𝐴, 𝐵} |
3 | | ffvelcdm 7083 |
. . . . . 6
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ∈ {𝐴, 𝐵}) → (𝐹‘𝐴) ∈ 𝑅) |
4 | 2, 3 | mpan2 689 |
. . . . 5
⊢ (𝐹:{𝐴, 𝐵}⟶𝑅 → (𝐹‘𝐴) ∈ 𝑅) |
5 | 4 | adantr 481 |
. . . 4
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → (𝐹‘𝐴) ∈ 𝑅) |
6 | | fprb.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
7 | 6 | prid2 4767 |
. . . . . 6
⊢ 𝐵 ∈ {𝐴, 𝐵} |
8 | | ffvelcdm 7083 |
. . . . . 6
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐵 ∈ {𝐴, 𝐵}) → (𝐹‘𝐵) ∈ 𝑅) |
9 | 7, 8 | mpan2 689 |
. . . . 5
⊢ (𝐹:{𝐴, 𝐵}⟶𝑅 → (𝐹‘𝐵) ∈ 𝑅) |
10 | 9 | adantr 481 |
. . . 4
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → (𝐹‘𝐵) ∈ 𝑅) |
11 | | fvex 6904 |
. . . . . . . 8
⊢ (𝐹‘𝐴) ∈ V |
12 | 1, 11 | fvpr1 7190 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) = (𝐹‘𝐴)) |
13 | | fvex 6904 |
. . . . . . . 8
⊢ (𝐹‘𝐵) ∈ V |
14 | 6, 13 | fvpr2 7192 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) = (𝐹‘𝐵)) |
15 | | fveq2 6891 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
16 | | fveq2 6891 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴)) |
17 | 15, 16 | eqeq12d 2748 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) ↔ (𝐹‘𝐴) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴))) |
18 | | eqcom 2739 |
. . . . . . . . 9
⊢ ((𝐹‘𝐴) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) ↔ ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) = (𝐹‘𝐴)) |
19 | 17, 18 | bitrdi 286 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) ↔ ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) = (𝐹‘𝐴))) |
20 | | fveq2 6891 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
21 | | fveq2 6891 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵)) |
22 | 20, 21 | eqeq12d 2748 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) ↔ (𝐹‘𝐵) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵))) |
23 | | eqcom 2739 |
. . . . . . . . 9
⊢ ((𝐹‘𝐵) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) ↔ ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) = (𝐹‘𝐵)) |
24 | 22, 23 | bitrdi 286 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) ↔ ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) = (𝐹‘𝐵))) |
25 | 1, 6, 19, 24 | ralpr 4704 |
. . . . . . 7
⊢
(∀𝑥 ∈
{𝐴, 𝐵} (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥) ↔ (({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐴) = (𝐹‘𝐴) ∧ ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝐵) = (𝐹‘𝐵))) |
26 | 12, 14, 25 | sylanbrc 583 |
. . . . . 6
⊢ (𝐴 ≠ 𝐵 → ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)) |
27 | 26 | adantl 482 |
. . . . 5
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥)) |
28 | | ffn 6717 |
. . . . . 6
⊢ (𝐹:{𝐴, 𝐵}⟶𝑅 → 𝐹 Fn {𝐴, 𝐵}) |
29 | 1, 6, 11, 13 | fpr 7151 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}:{𝐴, 𝐵}⟶{(𝐹‘𝐴), (𝐹‘𝐵)}) |
30 | 29 | ffnd 6718 |
. . . . . 6
⊢ (𝐴 ≠ 𝐵 → {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵}) |
31 | | eqfnfv 7032 |
. . . . . 6
⊢ ((𝐹 Fn {𝐴, 𝐵} ∧ {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} Fn {𝐴, 𝐵}) → (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ↔ ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥))) |
32 | 28, 30, 31 | syl2an 596 |
. . . . 5
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩} ↔ ∀𝑥 ∈ {𝐴, 𝐵} (𝐹‘𝑥) = ({⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}‘𝑥))) |
33 | 27, 32 | mpbird 256 |
. . . 4
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}) |
34 | | opeq2 4874 |
. . . . . . 7
⊢ (𝑥 = (𝐹‘𝐴) → ⟨𝐴, 𝑥⟩ = ⟨𝐴, (𝐹‘𝐴)⟩) |
35 | 34 | preq1d 4743 |
. . . . . 6
⊢ (𝑥 = (𝐹‘𝐴) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, 𝑦⟩}) |
36 | 35 | eqeq2d 2743 |
. . . . 5
⊢ (𝑥 = (𝐹‘𝐴) → (𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, 𝑦⟩})) |
37 | | opeq2 4874 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝐵) → ⟨𝐵, 𝑦⟩ = ⟨𝐵, (𝐹‘𝐵)⟩) |
38 | 37 | preq2d 4744 |
. . . . . 6
⊢ (𝑦 = (𝐹‘𝐵) → {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, 𝑦⟩} = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}) |
39 | 38 | eqeq2d 2743 |
. . . . 5
⊢ (𝑦 = (𝐹‘𝐵) → (𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, 𝑦⟩} ↔ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩})) |
40 | 36, 39 | rspc2ev 3624 |
. . . 4
⊢ (((𝐹‘𝐴) ∈ 𝑅 ∧ (𝐹‘𝐵) ∈ 𝑅 ∧ 𝐹 = {⟨𝐴, (𝐹‘𝐴)⟩, ⟨𝐵, (𝐹‘𝐵)⟩}) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}) |
41 | 5, 10, 33, 40 | syl3anc 1371 |
. . 3
⊢ ((𝐹:{𝐴, 𝐵}⟶𝑅 ∧ 𝐴 ≠ 𝐵) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}) |
42 | 41 | expcom 414 |
. 2
⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩})) |
43 | | vex 3478 |
. . . . . . 7
⊢ 𝑥 ∈ V |
44 | | vex 3478 |
. . . . . . 7
⊢ 𝑦 ∈ V |
45 | 1, 6, 43, 44 | fpr 7151 |
. . . . . 6
⊢ (𝐴 ≠ 𝐵 → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}⟶{𝑥, 𝑦}) |
46 | | prssi 4824 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → {𝑥, 𝑦} ⊆ 𝑅) |
47 | | fss 6734 |
. . . . . 6
⊢
(({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}⟶{𝑥, 𝑦} ∧ {𝑥, 𝑦} ⊆ 𝑅) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}⟶𝑅) |
48 | 45, 46, 47 | syl2an 596 |
. . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}⟶𝑅) |
49 | 48 | ex 413 |
. . . 4
⊢ (𝐴 ≠ 𝐵 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}⟶𝑅)) |
50 | | feq1 6698 |
. . . . 5
⊢ (𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}⟶𝑅)) |
51 | 50 | biimprcd 249 |
. . . 4
⊢
({⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩}:{𝐴, 𝐵}⟶𝑅 → (𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → 𝐹:{𝐴, 𝐵}⟶𝑅)) |
52 | 49, 51 | syl6 35 |
. . 3
⊢ (𝐴 ≠ 𝐵 → ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) → (𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → 𝐹:{𝐴, 𝐵}⟶𝑅))) |
53 | 52 | rexlimdvv 3210 |
. 2
⊢ (𝐴 ≠ 𝐵 → (∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩} → 𝐹:{𝐴, 𝐵}⟶𝑅)) |
54 | 42, 53 | impbid 211 |
1
⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {⟨𝐴, 𝑥⟩, ⟨𝐵, 𝑦⟩})) |