Step | Hyp | Ref
| Expression |
1 | | brex 4689 |
. . 3
⊢ (ARB → (A
∈ V ∧
B ∈
V)) |
2 | 1 | adantl 452 |
. 2
⊢ ((A ∈ C ∧ ARB) → (A
∈ V ∧
B ∈
V)) |
3 | | eleq1 2413 |
. . . . 5
⊢ (x = A →
(x ∈
C ↔ A ∈ C)) |
4 | | breq1 4642 |
. . . . 5
⊢ (x = A →
(xRy ↔
ARy)) |
5 | 3, 4 | anbi12d 691 |
. . . 4
⊢ (x = A →
((x ∈
C ∧
xRy) ↔
(A ∈
C ∧
ARy))) |
6 | 5 | imbi1d 308 |
. . 3
⊢ (x = A →
(((x ∈
C ∧
xRy) →
y ∈
C) ↔ ((A ∈ C ∧ ARy) → y
∈ C))) |
7 | | breq2 4643 |
. . . . 5
⊢ (y = B →
(ARy ↔
ARB)) |
8 | 7 | anbi2d 684 |
. . . 4
⊢ (y = B →
((A ∈
C ∧
ARy) ↔
(A ∈
C ∧
ARB))) |
9 | | eleq1 2413 |
. . . 4
⊢ (y = B →
(y ∈
C ↔ B ∈ C)) |
10 | 8, 9 | imbi12d 311 |
. . 3
⊢ (y = B →
(((A ∈
C ∧
ARy) →
y ∈
C) ↔ ((A ∈ C ∧ ARB) → B
∈ C))) |
11 | | breq1 4642 |
. . . . . . . . . . . . . 14
⊢ (z = x →
(zRy ↔
xRy)) |
12 | 11 | rspcev 2955 |
. . . . . . . . . . . . 13
⊢ ((x ∈ a ∧ xRy) → ∃z ∈ a zRy) |
13 | | elima 4754 |
. . . . . . . . . . . . 13
⊢ (y ∈ (R “ a)
↔ ∃z ∈ a zRy) |
14 | 12, 13 | sylibr 203 |
. . . . . . . . . . . 12
⊢ ((x ∈ a ∧ xRy) → y
∈ (R
“ a)) |
15 | 14 | ancoms 439 |
. . . . . . . . . . 11
⊢ ((xRy ∧ x ∈ a) → y
∈ (R
“ a)) |
16 | | ssel 3267 |
. . . . . . . . . . 11
⊢ ((R “ a)
⊆ a
→ (y ∈ (R “
a) → y ∈ a)) |
17 | 15, 16 | syl5 28 |
. . . . . . . . . 10
⊢ ((R “ a)
⊆ a
→ ((xRy ∧ x ∈ a) →
y ∈
a)) |
18 | 17 | exp3a 425 |
. . . . . . . . 9
⊢ ((R “ a)
⊆ a
→ (xRy →
(x ∈
a → y ∈ a))) |
19 | 18 | com12 27 |
. . . . . . . 8
⊢ (xRy → ((R
“ a) ⊆ a →
(x ∈
a → y ∈ a))) |
20 | 19 | adantld 453 |
. . . . . . 7
⊢ (xRy → ((S
⊆ a
∧ (R
“ a) ⊆ a) →
(x ∈
a → y ∈ a))) |
21 | 20 | a2d 23 |
. . . . . 6
⊢ (xRy → (((S
⊆ a
∧ (R
“ a) ⊆ a) →
x ∈
a) → ((S ⊆ a ∧ (R “ a)
⊆ a)
→ y ∈ a))) |
22 | 21 | alimdv 1621 |
. . . . 5
⊢ (xRy → (∀a((S ⊆ a ∧ (R “ a)
⊆ a)
→ x ∈ a) →
∀a((S ⊆ a ∧ (R “
a) ⊆
a) → y ∈ a))) |
23 | | clos1base.1 |
. . . . . . . 8
⊢ C = Clos1 (S, R) |
24 | | df-clos1 5873 |
. . . . . . . 8
⊢ Clos1 (S, R) = ∩{a ∣ (S ⊆ a ∧ (R “ a)
⊆ a)} |
25 | 23, 24 | eqtri 2373 |
. . . . . . 7
⊢ C = ∩{a ∣ (S ⊆ a ∧ (R “ a)
⊆ a)} |
26 | 25 | eleq2i 2417 |
. . . . . 6
⊢ (x ∈ C ↔ x ∈ ∩{a ∣ (S ⊆ a ∧ (R “ a)
⊆ a)}) |
27 | | vex 2862 |
. . . . . . 7
⊢ x ∈
V |
28 | 27 | elintab 3937 |
. . . . . 6
⊢ (x ∈ ∩{a ∣ (S ⊆ a ∧ (R “
a) ⊆
a)} ↔ ∀a((S ⊆ a ∧ (R “ a)
⊆ a)
→ x ∈ a)) |
29 | 26, 28 | bitri 240 |
. . . . 5
⊢ (x ∈ C ↔ ∀a((S ⊆ a ∧ (R “ a)
⊆ a)
→ x ∈ a)) |
30 | 25 | eleq2i 2417 |
. . . . . 6
⊢ (y ∈ C ↔ y ∈ ∩{a ∣ (S ⊆ a ∧ (R “ a)
⊆ a)}) |
31 | | vex 2862 |
. . . . . . 7
⊢ y ∈
V |
32 | 31 | elintab 3937 |
. . . . . 6
⊢ (y ∈ ∩{a ∣ (S ⊆ a ∧ (R “
a) ⊆
a)} ↔ ∀a((S ⊆ a ∧ (R “ a)
⊆ a)
→ y ∈ a)) |
33 | 30, 32 | bitri 240 |
. . . . 5
⊢ (y ∈ C ↔ ∀a((S ⊆ a ∧ (R “ a)
⊆ a)
→ y ∈ a)) |
34 | 22, 29, 33 | 3imtr4g 261 |
. . . 4
⊢ (xRy → (x
∈ C
→ y ∈ C)) |
35 | 34 | impcom 419 |
. . 3
⊢ ((x ∈ C ∧ xRy) → y
∈ C) |
36 | 6, 10, 35 | vtocl2g 2918 |
. 2
⊢ ((A ∈ V ∧ B ∈ V) → ((A
∈ C ∧ ARB) →
B ∈
C)) |
37 | 2, 36 | mpcom 32 |
1
⊢ ((A ∈ C ∧ ARB) → B
∈ C) |