Proof of Theorem oprabval
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | eleq1 1149 |
. . . . . . . . 9
⊢ (x =
A → (x ∈ R
↔ A ∈ R)) |
| 2 | 1 | anbi1d 469 |
. . . . . . . 8
⊢ (x =
A → ((x ∈ R ∧
y ∈ S) ↔ (A
∈ R ∧ y ∈ S))) |
| 3 | | eleq1 1149 |
. . . . . . . . 9
⊢ (y =
B → (y ∈ S
↔ B ∈ S)) |
| 4 | 3 | anbi2d 468 |
. . . . . . . 8
⊢ (y =
B → ((A ∈ R ∧
y ∈ S) ↔ (A
∈ R ∧ B ∈ S))) |
| 5 | 2, 4 | opelopabg 2115 |
. . . . . . 7
⊢ ((A
∈ R ∧ B ∈ S)
→ (⟨A, B⟩ ∈ {⟨x, y⟩∣(x
∈ R ∧ y ∈ S)}
↔ (A ∈ R ∧ B ∈
S))) |
| 6 | 5 | biimprd 136 |
. . . . . 6
⊢ ((A
∈ R ∧ B ∈ S)
→ ((A ∈ R ∧ B ∈
S) → ⟨A, B⟩
∈ {⟨x, y⟩∣(x
∈ R ∧ y ∈ S)})) |
| 7 | 6 | pm2.43i 58 |
. . . . 5
⊢ ((A
∈ R ∧ B ∈ S)
→ ⟨A, B⟩ ∈ {⟨x, y⟩∣(x
∈ R ∧ y ∈ S)}) |
| 8 | | oprabval.5 |
. . . . . . 7
⊢ ((x
∈ R ∧ y ∈ S)
→ ∃!zφ) |
| 9 | 8 | fnoprab 3038 |
. . . . . 6
⊢ {⟨⟨x, y⟩,
z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)}
Fn {⟨x, y⟩∣(x
∈ R ∧ y ∈ S)} |
| 10 | | oprabval.1 |
. . . . . . 7
⊢ C
∈ V |
| 11 | 10 | fnfvop 2856 |
. . . . . 6
⊢ (({⟨⟨x, y⟩,
z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)}
Fn {⟨x, y⟩∣(x
∈ R ∧ y ∈ S)}
∧ ⟨A, B⟩ ∈ {⟨x, y⟩∣(x
∈ R ∧ y ∈ S)})
→ (({⟨⟨x, y⟩, z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)}
‘⟨A, B⟩) = C
↔ ⟨⟨A, B⟩, C⟩
∈ {⟨⟨x, y⟩, z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)})) |
| 12 | 9, 11 | mpan 518 |
. . . . 5
⊢ (⟨A, B⟩
∈ {⟨x, y⟩∣(x
∈ R ∧ y ∈ S)}
→ (({⟨⟨x, y⟩, z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)}
‘⟨A, B⟩) = C
↔ ⟨⟨A, B⟩, C⟩
∈ {⟨⟨x, y⟩, z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)})) |
| 13 | 7, 12 | syl 12 |
. . . 4
⊢ ((A
∈ R ∧ B ∈ S)
→ (({⟨⟨x, y⟩, z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)}
‘⟨A, B⟩) = C
↔ ⟨⟨A, B⟩, C⟩
∈ {⟨⟨x, y⟩, z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)})) |
| 14 | | oprabval.2 |
. . . . . . 7
⊢ (x =
A → (φ ↔ ψ)) |
| 15 | 2, 14 | anbi12d 476 |
. . . . . 6
⊢ (x =
A → (((x ∈ R ∧
y ∈ S) ∧ φ)
↔ ((A ∈ R ∧ y ∈
S) ∧ ψ))) |
| 16 | | oprabval.3 |
. . . . . . 7
⊢ (y =
B → (ψ ↔ χ)) |
| 17 | 4, 16 | anbi12d 476 |
. . . . . 6
⊢ (y =
B → (((A ∈ R ∧
y ∈ S) ∧ ψ)
↔ ((A ∈ R ∧ B ∈
S) ∧ χ))) |
| 18 | | oprabval.4 |
. . . . . . 7
⊢ (z =
C → (χ ↔ θ)) |
| 19 | 18 | anbi2d 468 |
. . . . . 6
⊢ (z =
C → (((A ∈ R ∧
B ∈ S) ∧ χ)
↔ ((A ∈ R ∧ B ∈
S) ∧ θ))) |
| 20 | 15, 17, 19 | eloprabg 3035 |
. . . . 5
⊢ ((A
∈ R ∧ B ∈ S ∧
C ∈ V) →
(⟨⟨A, B⟩, C⟩
∈ {⟨⟨x, y⟩, z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)}
↔ ((A ∈ R ∧ B ∈
S) ∧ θ))) |
| 21 | 10, 20 | mp3an3 641 |
. . . 4
⊢ ((A
∈ R ∧ B ∈ S)
→ (⟨⟨A, B⟩, C⟩
∈ {⟨⟨x, y⟩, z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)}
↔ ((A ∈ R ∧ B ∈
S) ∧ θ))) |
| 22 | 13, 21 | bitrd 406 |
. . 3
⊢ ((A
∈ R ∧ B ∈ S)
→ (({⟨⟨x, y⟩, z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)}
‘⟨A, B⟩) = C
↔ ((A ∈ R ∧ B ∈
S) ∧ θ))) |
| 23 | | df-opr 3003 |
. . . . 5
⊢ (AFB) = (F
‘⟨A, B⟩) |
| 24 | | oprabval.6 |
. . . . . 6
⊢ F =
{⟨⟨x, y⟩, z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)} |
| 25 | 24 | fveq1i 2833 |
. . . . 5
⊢ (F
‘⟨A, B⟩) = ({⟨⟨x, y⟩,
z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)}
‘⟨A, B⟩) |
| 26 | 23, 25 | eqtr 1119 |
. . . 4
⊢ (AFB) = ({⟨⟨x, y⟩,
z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)}
‘⟨A, B⟩) |
| 27 | 26 | cleq1i 1108 |
. . 3
⊢ ((AFB) = C ↔
({⟨⟨x, y⟩, z⟩∣((x ∈ R ∧
y ∈ S) ∧ φ)}
‘⟨A, B⟩) = C) |
| 28 | 22, 27 | syl5bb 410 |
. 2
⊢ ((A
∈ R ∧ B ∈ S)
→ ((AFB) = C ↔ ((A
∈ R ∧ B ∈ S)
∧ θ))) |
| 29 | | ibar 487 |
. 2
⊢ ((A
∈ R ∧ B ∈ S)
→ (θ ↔ ((A ∈ R ∧
B ∈ S) ∧ θ))) |
| 30 | 28, 29 | bitr4d 409 |
1
⊢ ((A
∈ R ∧ B ∈ S)
→ ((AFB) = C ↔ θ)) |
Home