| Step | Hyp | Ref
| Expression |
| 1 | | erex 8769 |
. . . . . . 7
⊢ (𝑅 Er 𝐴 → (𝐴 ∈ 𝑉 → 𝑅 ∈ V)) |
| 2 | 1 | impcom 407 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) → 𝑅 ∈ V) |
| 3 | | ecexg 8749 |
. . . . . 6
⊢ (𝑅 ∈ V → [𝑢]𝑅 ∈ V) |
| 4 | 2, 3 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) → [𝑢]𝑅 ∈ V) |
| 5 | 4 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑢 ∈ 𝐴) → [𝑢]𝑅 ∈ V) |
| 6 | 5 | ralrimiva 3146 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) → ∀𝑢 ∈ 𝐴 [𝑢]𝑅 ∈ V) |
| 7 | | eqid 2737 |
. . . 4
⊢ (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) = (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) |
| 8 | 7 | fnmpt 6708 |
. . 3
⊢
(∀𝑢 ∈
𝐴 [𝑢]𝑅 ∈ V → (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) Fn 𝐴) |
| 9 | 6, 8 | syl 17 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) → (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) Fn 𝐴) |
| 10 | | simpllr 776 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑅 Er 𝐴) |
| 11 | | simpr 484 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 12 | 11 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 13 | 10, 12 | erth 8796 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ↔ [𝑥]𝑅 = [𝑦]𝑅)) |
| 14 | | eceq1 8784 |
. . . . . . . 8
⊢ (𝑢 = 𝑥 → [𝑢]𝑅 = [𝑥]𝑅) |
| 15 | | ecelqsg 8812 |
. . . . . . . . 9
⊢ ((𝑅 ∈ V ∧ 𝑥 ∈ 𝐴) → [𝑥]𝑅 ∈ (𝐴 / 𝑅)) |
| 16 | 2, 15 | sylan 580 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑥 ∈ 𝐴) → [𝑥]𝑅 ∈ (𝐴 / 𝑅)) |
| 17 | 7, 14, 11, 16 | fvmptd3 7039 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑥 ∈ 𝐴) → ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥) = [𝑥]𝑅) |
| 18 | 17 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥) = [𝑥]𝑅) |
| 19 | | eceq1 8784 |
. . . . . . . 8
⊢ (𝑢 = 𝑦 → [𝑢]𝑅 = [𝑦]𝑅) |
| 20 | | simpr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
| 21 | | ecelqsg 8812 |
. . . . . . . . 9
⊢ ((𝑅 ∈ V ∧ 𝑦 ∈ 𝐴) → [𝑦]𝑅 ∈ (𝐴 / 𝑅)) |
| 22 | 2, 21 | sylan 580 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑦 ∈ 𝐴) → [𝑦]𝑅 ∈ (𝐴 / 𝑅)) |
| 23 | 7, 19, 20, 22 | fvmptd3 7039 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑦 ∈ 𝐴) → ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦) = [𝑦]𝑅) |
| 24 | 23 | adantlr 715 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦) = [𝑦]𝑅) |
| 25 | 18, 24 | eqeq12d 2753 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦) ↔ [𝑥]𝑅 = [𝑦]𝑅)) |
| 26 | 13, 25 | bitr4d 282 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ↔ ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦))) |
| 27 | 26 | ralrimiva 3146 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦))) |
| 28 | 27 | ralrimiva 3146 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦))) |
| 29 | | mptexg 7241 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) ∈ V) |
| 30 | 29 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) → (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) ∈ V) |
| 31 | | fneq1 6659 |
. . . . 5
⊢ (𝑓 = (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) → (𝑓 Fn 𝐴 ↔ (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) Fn 𝐴)) |
| 32 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑓 = (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → 𝑓 = (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)) |
| 33 | 32 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝑓 = (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑓‘𝑥) = ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥)) |
| 34 | 32 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝑓 = (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑓‘𝑦) = ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦)) |
| 35 | 33, 34 | eqeq12d 2753 |
. . . . . . 7
⊢ ((𝑓 = (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑓‘𝑥) = (𝑓‘𝑦) ↔ ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦))) |
| 36 | 35 | bibi2d 342 |
. . . . . 6
⊢ ((𝑓 = (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑥𝑅𝑦 ↔ (𝑓‘𝑥) = (𝑓‘𝑦)) ↔ (𝑥𝑅𝑦 ↔ ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦)))) |
| 37 | 36 | 2ralbidva 3219 |
. . . . 5
⊢ (𝑓 = (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝑓‘𝑥) = (𝑓‘𝑦)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦)))) |
| 38 | 31, 37 | anbi12d 632 |
. . . 4
⊢ (𝑓 = (𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) → ((𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝑓‘𝑥) = (𝑓‘𝑦))) ↔ ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦))))) |
| 39 | 38 | spcegv 3597 |
. . 3
⊢ ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) ∈ V → (((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝑓‘𝑥) = (𝑓‘𝑦))))) |
| 40 | 30, 39 | syl 17 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) → (((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑥) = ((𝑢 ∈ 𝐴 ↦ [𝑢]𝑅)‘𝑦))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝑓‘𝑥) = (𝑓‘𝑦))))) |
| 41 | 9, 28, 40 | mp2and 699 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 Er 𝐴) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝑓‘𝑥) = (𝑓‘𝑦)))) |