Step | Hyp | Ref
| Expression |
1 | | nfv 1521 |
. . 3
⊢
Ⅎ𝑥𝜑 |
2 | | flift.1 |
. . . . 5
⊢ 𝐹 = ran (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) |
3 | | nfmpt1 4080 |
. . . . . 6
⊢
Ⅎ𝑥(𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) |
4 | 3 | nfrn 4854 |
. . . . 5
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) |
5 | 2, 4 | nfcxfr 2309 |
. . . 4
⊢
Ⅎ𝑥𝐹 |
6 | 5 | nffun 5219 |
. . 3
⊢
Ⅎ𝑥Fun 𝐹 |
7 | | fveq2 5494 |
. . . . . . 7
⊢ (𝐴 = 𝐶 → (𝐹‘𝐴) = (𝐹‘𝐶)) |
8 | | simplr 525 |
. . . . . . . . 9
⊢ (((𝜑 ∧ Fun 𝐹) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → Fun 𝐹) |
9 | | flift.2 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑅) |
10 | | flift.3 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐵 ∈ 𝑆) |
11 | 2, 9, 10 | fliftel1 5771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴𝐹𝐵) |
12 | 11 | ad2ant2r 506 |
. . . . . . . . 9
⊢ (((𝜑 ∧ Fun 𝐹) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐴𝐹𝐵) |
13 | | funbrfv 5533 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (𝐴𝐹𝐵 → (𝐹‘𝐴) = 𝐵)) |
14 | 8, 12, 13 | sylc 62 |
. . . . . . . 8
⊢ (((𝜑 ∧ Fun 𝐹) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘𝐴) = 𝐵) |
15 | | simprr 527 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ Fun 𝐹) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
16 | | eqidd 2171 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ Fun 𝐹) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐶 = 𝐶) |
17 | | eqidd 2171 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ Fun 𝐹) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐷 = 𝐷) |
18 | | fliftfun.4 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐶) |
19 | 18 | eqeq2d 2182 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐶)) |
20 | | fliftfun.5 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐷) |
21 | 20 | eqeq2d 2182 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝐷 = 𝐵 ↔ 𝐷 = 𝐷)) |
22 | 19, 21 | anbi12d 470 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝐶 = 𝐴 ∧ 𝐷 = 𝐵) ↔ (𝐶 = 𝐶 ∧ 𝐷 = 𝐷))) |
23 | 22 | rspcev 2834 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑋 ∧ (𝐶 = 𝐶 ∧ 𝐷 = 𝐷)) → ∃𝑥 ∈ 𝑋 (𝐶 = 𝐴 ∧ 𝐷 = 𝐵)) |
24 | 15, 16, 17, 23 | syl12anc 1231 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ Fun 𝐹) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ∃𝑥 ∈ 𝑋 (𝐶 = 𝐴 ∧ 𝐷 = 𝐵)) |
25 | 2, 9, 10 | fliftel 5770 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶 = 𝐴 ∧ 𝐷 = 𝐵))) |
26 | 25 | ad2antrr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ Fun 𝐹) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐶𝐹𝐷 ↔ ∃𝑥 ∈ 𝑋 (𝐶 = 𝐴 ∧ 𝐷 = 𝐵))) |
27 | 24, 26 | mpbird 166 |
. . . . . . . . 9
⊢ (((𝜑 ∧ Fun 𝐹) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → 𝐶𝐹𝐷) |
28 | | funbrfv 5533 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (𝐶𝐹𝐷 → (𝐹‘𝐶) = 𝐷)) |
29 | 8, 27, 28 | sylc 62 |
. . . . . . . 8
⊢ (((𝜑 ∧ Fun 𝐹) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘𝐶) = 𝐷) |
30 | 14, 29 | eqeq12d 2185 |
. . . . . . 7
⊢ (((𝜑 ∧ Fun 𝐹) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝐴) = (𝐹‘𝐶) ↔ 𝐵 = 𝐷)) |
31 | 7, 30 | syl5ib 153 |
. . . . . 6
⊢ (((𝜑 ∧ Fun 𝐹) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐴 = 𝐶 → 𝐵 = 𝐷)) |
32 | 31 | anassrs 398 |
. . . . 5
⊢ ((((𝜑 ∧ Fun 𝐹) ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑋) → (𝐴 = 𝐶 → 𝐵 = 𝐷)) |
33 | 32 | ralrimiva 2543 |
. . . 4
⊢ (((𝜑 ∧ Fun 𝐹) ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷)) |
34 | 33 | exp31 362 |
. . 3
⊢ (𝜑 → (Fun 𝐹 → (𝑥 ∈ 𝑋 → ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷)))) |
35 | 1, 6, 34 | ralrimd 2548 |
. 2
⊢ (𝜑 → (Fun 𝐹 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷))) |
36 | 2, 9, 10 | fliftel 5770 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧𝐹𝑢 ↔ ∃𝑥 ∈ 𝑋 (𝑧 = 𝐴 ∧ 𝑢 = 𝐵))) |
37 | 2, 9, 10 | fliftel 5770 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑧𝐹𝑣 ↔ ∃𝑥 ∈ 𝑋 (𝑧 = 𝐴 ∧ 𝑣 = 𝐵))) |
38 | 18 | eqeq2d 2182 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑧 = 𝐴 ↔ 𝑧 = 𝐶)) |
39 | 20 | eqeq2d 2182 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝑣 = 𝐵 ↔ 𝑣 = 𝐷)) |
40 | 38, 39 | anbi12d 470 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ((𝑧 = 𝐴 ∧ 𝑣 = 𝐵) ↔ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) |
41 | 40 | cbvrexv 2697 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝑋 (𝑧 = 𝐴 ∧ 𝑣 = 𝐵) ↔ ∃𝑦 ∈ 𝑋 (𝑧 = 𝐶 ∧ 𝑣 = 𝐷)) |
42 | 37, 41 | bitrdi 195 |
. . . . . . . . 9
⊢ (𝜑 → (𝑧𝐹𝑣 ↔ ∃𝑦 ∈ 𝑋 (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) |
43 | 36, 42 | anbi12d 470 |
. . . . . . . 8
⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑧𝐹𝑣) ↔ (∃𝑥 ∈ 𝑋 (𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ ∃𝑦 ∈ 𝑋 (𝑧 = 𝐶 ∧ 𝑣 = 𝐷)))) |
44 | 43 | biimpd 143 |
. . . . . . 7
⊢ (𝜑 → ((𝑧𝐹𝑢 ∧ 𝑧𝐹𝑣) → (∃𝑥 ∈ 𝑋 (𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ ∃𝑦 ∈ 𝑋 (𝑧 = 𝐶 ∧ 𝑣 = 𝐷)))) |
45 | | reeanv 2639 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝑋 ∃𝑦 ∈ 𝑋 ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷)) ↔ (∃𝑥 ∈ 𝑋 (𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ ∃𝑦 ∈ 𝑋 (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) |
46 | | r19.29 2607 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) ∧ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) → ∃𝑥 ∈ 𝑋 (∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) ∧ ∃𝑦 ∈ 𝑋 ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷)))) |
47 | | r19.29 2607 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) ∧ ∃𝑦 ∈ 𝑋 ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) → ∃𝑦 ∈ 𝑋 ((𝐴 = 𝐶 → 𝐵 = 𝐷) ∧ ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷)))) |
48 | | eqtr2 2189 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 = 𝐴 ∧ 𝑧 = 𝐶) → 𝐴 = 𝐶) |
49 | 48 | ad2ant2r 506 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷)) → 𝐴 = 𝐶) |
50 | 49 | imim1i 60 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 = 𝐶 → 𝐵 = 𝐷) → (((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷)) → 𝐵 = 𝐷)) |
51 | 50 | imp 123 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 = 𝐶 → 𝐵 = 𝐷) ∧ ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) → 𝐵 = 𝐷) |
52 | | simprlr 533 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 = 𝐶 → 𝐵 = 𝐷) ∧ ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) → 𝑢 = 𝐵) |
53 | | simprrr 535 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 = 𝐶 → 𝐵 = 𝐷) ∧ ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) → 𝑣 = 𝐷) |
54 | 51, 52, 53 | 3eqtr4d 2213 |
. . . . . . . . . . . . 13
⊢ (((𝐴 = 𝐶 → 𝐵 = 𝐷) ∧ ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) → 𝑢 = 𝑣) |
55 | 54 | rexlimivw 2583 |
. . . . . . . . . . . 12
⊢
(∃𝑦 ∈
𝑋 ((𝐴 = 𝐶 → 𝐵 = 𝐷) ∧ ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) → 𝑢 = 𝑣) |
56 | 47, 55 | syl 14 |
. . . . . . . . . . 11
⊢
((∀𝑦 ∈
𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) ∧ ∃𝑦 ∈ 𝑋 ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) → 𝑢 = 𝑣) |
57 | 56 | rexlimivw 2583 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝑋 (∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) ∧ ∃𝑦 ∈ 𝑋 ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) → 𝑢 = 𝑣) |
58 | 46, 57 | syl 14 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) ∧ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷))) → 𝑢 = 𝑣) |
59 | 58 | ex 114 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) → (∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑋 ((𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑣 = 𝐷)) → 𝑢 = 𝑣)) |
60 | 45, 59 | syl5bir 152 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) → ((∃𝑥 ∈ 𝑋 (𝑧 = 𝐴 ∧ 𝑢 = 𝐵) ∧ ∃𝑦 ∈ 𝑋 (𝑧 = 𝐶 ∧ 𝑣 = 𝐷)) → 𝑢 = 𝑣)) |
61 | 44, 60 | syl9 72 |
. . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) → ((𝑧𝐹𝑢 ∧ 𝑧𝐹𝑣) → 𝑢 = 𝑣))) |
62 | 61 | alrimdv 1869 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) → ∀𝑣((𝑧𝐹𝑢 ∧ 𝑧𝐹𝑣) → 𝑢 = 𝑣))) |
63 | 62 | alrimdv 1869 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) → ∀𝑢∀𝑣((𝑧𝐹𝑢 ∧ 𝑧𝐹𝑣) → 𝑢 = 𝑣))) |
64 | 63 | alrimdv 1869 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) → ∀𝑧∀𝑢∀𝑣((𝑧𝐹𝑢 ∧ 𝑧𝐹𝑣) → 𝑢 = 𝑣))) |
65 | 2, 9, 10 | fliftrel 5769 |
. . . . 5
⊢ (𝜑 → 𝐹 ⊆ (𝑅 × 𝑆)) |
66 | | relxp 4718 |
. . . . 5
⊢ Rel
(𝑅 × 𝑆) |
67 | | relss 4696 |
. . . . 5
⊢ (𝐹 ⊆ (𝑅 × 𝑆) → (Rel (𝑅 × 𝑆) → Rel 𝐹)) |
68 | 65, 66, 67 | mpisyl 1439 |
. . . 4
⊢ (𝜑 → Rel 𝐹) |
69 | | dffun2 5206 |
. . . . 5
⊢ (Fun
𝐹 ↔ (Rel 𝐹 ∧ ∀𝑧∀𝑢∀𝑣((𝑧𝐹𝑢 ∧ 𝑧𝐹𝑣) → 𝑢 = 𝑣))) |
70 | 69 | baib 914 |
. . . 4
⊢ (Rel
𝐹 → (Fun 𝐹 ↔ ∀𝑧∀𝑢∀𝑣((𝑧𝐹𝑢 ∧ 𝑧𝐹𝑣) → 𝑢 = 𝑣))) |
71 | 68, 70 | syl 14 |
. . 3
⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑧∀𝑢∀𝑣((𝑧𝐹𝑢 ∧ 𝑧𝐹𝑣) → 𝑢 = 𝑣))) |
72 | 64, 71 | sylibrd 168 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷) → Fun 𝐹)) |
73 | 35, 72 | impbid 128 |
1
⊢ (𝜑 → (Fun 𝐹 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐴 = 𝐶 → 𝐵 = 𝐷))) |