Step | Hyp | Ref
| Expression |
1 | | funrel 4862 |
. . . . 5
⊢ (Fun
f → Rel f) |
2 | 1 | adantr 261 |
. . . 4
⊢ ((Fun
f ∧ ∀g ∈ A (f ⊆ g
∨ g
⊆ f)) → Rel f) |
3 | 2 | ralimi 2378 |
. . 3
⊢ (∀f ∈ A (Fun
f ∧ ∀g ∈ A (f ⊆ g
∨ g
⊆ f)) → ∀f ∈ A Rel
f) |
4 | | reluni 4403 |
. . 3
⊢ (Rel
∪ A ↔ ∀f ∈ A Rel
f) |
5 | 3, 4 | sylibr 137 |
. 2
⊢ (∀f ∈ A (Fun
f ∧ ∀g ∈ A (f ⊆ g
∨ g
⊆ f)) → Rel ∪ A) |
6 | | r19.28av 2443 |
. . . 4
⊢ ((Fun
f ∧ ∀g ∈ A (f ⊆ g
∨ g
⊆ f)) → ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f))) |
7 | 6 | ralimi 2378 |
. . 3
⊢ (∀f ∈ A (Fun
f ∧ ∀g ∈ A (f ⊆ g
∨ g
⊆ f)) → ∀f ∈ A ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f))) |
8 | | ssel 2933 |
. . . . . . . . . . . . 13
⊢ (w ⊆ v
→ (〈x, y〉 ∈ w → 〈x, y〉 ∈ v)) |
9 | 8 | anim1d 319 |
. . . . . . . . . . . 12
⊢ (w ⊆ v
→ ((〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v) →
(〈x, y〉 ∈ v ∧ 〈x, z〉 ∈ v))) |
10 | | dffun4 4856 |
. . . . . . . . . . . . . . 15
⊢ (Fun
v ↔ (Rel v ∧ ∀x∀y∀z((〈x,
y〉 ∈
v ∧
〈x, z〉 ∈ v) → y =
z))) |
11 | 10 | simprbi 260 |
. . . . . . . . . . . . . 14
⊢ (Fun
v → ∀x∀y∀z((〈x,
y〉 ∈
v ∧
〈x, z〉 ∈ v) → y =
z)) |
12 | 11 | 19.21bbi 1448 |
. . . . . . . . . . . . 13
⊢ (Fun
v → ∀z((〈x,
y〉 ∈
v ∧
〈x, z〉 ∈ v) → y =
z)) |
13 | 12 | 19.21bi 1447 |
. . . . . . . . . . . 12
⊢ (Fun
v → ((〈x, y〉 ∈ v ∧ 〈x,
z〉 ∈
v) → y = z)) |
14 | 9, 13 | syl9r 67 |
. . . . . . . . . . 11
⊢ (Fun
v → (w ⊆ v
→ ((〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v) →
y = z))) |
15 | 14 | adantl 262 |
. . . . . . . . . 10
⊢ ((Fun
w ∧ Fun
v) → (w ⊆ v
→ ((〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v) →
y = z))) |
16 | | ssel 2933 |
. . . . . . . . . . . . 13
⊢ (v ⊆ w
→ (〈x, z〉 ∈ v → 〈x, z〉 ∈ w)) |
17 | 16 | anim2d 320 |
. . . . . . . . . . . 12
⊢ (v ⊆ w
→ ((〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v) →
(〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ w))) |
18 | | dffun4 4856 |
. . . . . . . . . . . . . . 15
⊢ (Fun
w ↔ (Rel w ∧ ∀x∀y∀z((〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ w) → y =
z))) |
19 | 18 | simprbi 260 |
. . . . . . . . . . . . . 14
⊢ (Fun
w → ∀x∀y∀z((〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ w) → y =
z)) |
20 | 19 | 19.21bbi 1448 |
. . . . . . . . . . . . 13
⊢ (Fun
w → ∀z((〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ w) → y =
z)) |
21 | 20 | 19.21bi 1447 |
. . . . . . . . . . . 12
⊢ (Fun
w → ((〈x, y〉 ∈ w ∧ 〈x,
z〉 ∈
w) → y = z)) |
22 | 17, 21 | syl9r 67 |
. . . . . . . . . . 11
⊢ (Fun
w → (v ⊆ w
→ ((〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v) →
y = z))) |
23 | 22 | adantr 261 |
. . . . . . . . . 10
⊢ ((Fun
w ∧ Fun
v) → (v ⊆ w
→ ((〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v) →
y = z))) |
24 | 15, 23 | jaod 636 |
. . . . . . . . 9
⊢ ((Fun
w ∧ Fun
v) → ((w ⊆ v
∨ v
⊆ w) → ((〈x, y〉 ∈ w ∧ 〈x,
z〉 ∈
v) → y = z))) |
25 | 24 | imp 115 |
. . . . . . . 8
⊢ (((Fun
w ∧ Fun
v) ∧
(w ⊆ v ∨ v ⊆ w))
→ ((〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v) →
y = z)) |
26 | 25 | ralimi 2378 |
. . . . . . 7
⊢ (∀v ∈ A ((Fun
w ∧ Fun
v) ∧
(w ⊆ v ∨ v ⊆ w))
→ ∀v ∈ A ((〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ v) → y =
z)) |
27 | 26 | ralimi 2378 |
. . . . . 6
⊢ (∀w ∈ A ∀v ∈ A ((Fun
w ∧ Fun
v) ∧
(w ⊆ v ∨ v ⊆ w))
→ ∀w ∈ A ∀v ∈ A ((〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ v) → y =
z)) |
28 | | funeq 4864 |
. . . . . . . . . 10
⊢ (f = w →
(Fun f ↔ Fun w)) |
29 | | sseq1 2960 |
. . . . . . . . . . 11
⊢ (f = w →
(f ⊆ g ↔ w
⊆ g)) |
30 | | sseq2 2961 |
. . . . . . . . . . 11
⊢ (f = w →
(g ⊆ f ↔ g
⊆ w)) |
31 | 29, 30 | orbi12d 706 |
. . . . . . . . . 10
⊢ (f = w →
((f ⊆ g ∨ g ⊆ f)
↔ (w ⊆ g ∨ g ⊆ w))) |
32 | 28, 31 | anbi12d 442 |
. . . . . . . . 9
⊢ (f = w →
((Fun f ∧
(f ⊆ g ∨ g ⊆ f))
↔ (Fun w ∧ (w ⊆
g ∨
g ⊆ w)))) |
33 | | sseq2 2961 |
. . . . . . . . . . 11
⊢ (g = v →
(w ⊆ g ↔ w
⊆ v)) |
34 | | sseq1 2960 |
. . . . . . . . . . 11
⊢ (g = v →
(g ⊆ w ↔ v
⊆ w)) |
35 | 33, 34 | orbi12d 706 |
. . . . . . . . . 10
⊢ (g = v →
((w ⊆ g ∨ g ⊆ w)
↔ (w ⊆ v ∨ v ⊆ w))) |
36 | 35 | anbi2d 437 |
. . . . . . . . 9
⊢ (g = v →
((Fun w ∧
(w ⊆ g ∨ g ⊆ w))
↔ (Fun w ∧ (w ⊆
v ∨
v ⊆ w)))) |
37 | 32, 36 | cbvral2v 2535 |
. . . . . . . 8
⊢ (∀f ∈ A ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f))
↔ ∀w ∈ A ∀v ∈ A (Fun w ∧ (w ⊆
v ∨
v ⊆ w))) |
38 | | ralcom 2467 |
. . . . . . . . 9
⊢ (∀f ∈ A ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f))
↔ ∀g ∈ A ∀f ∈ A (Fun f ∧ (f ⊆
g ∨
g ⊆ f))) |
39 | | orcom 646 |
. . . . . . . . . . . 12
⊢
((f ⊆ g ∨ g ⊆ f)
↔ (g ⊆ f ∨ f ⊆ g)) |
40 | | sseq1 2960 |
. . . . . . . . . . . . 13
⊢ (g = w →
(g ⊆ f ↔ w
⊆ f)) |
41 | | sseq2 2961 |
. . . . . . . . . . . . 13
⊢ (g = w →
(f ⊆ g ↔ f
⊆ w)) |
42 | 40, 41 | orbi12d 706 |
. . . . . . . . . . . 12
⊢ (g = w →
((g ⊆ f ∨ f ⊆ g)
↔ (w ⊆ f ∨ f ⊆ w))) |
43 | 39, 42 | syl5bb 181 |
. . . . . . . . . . 11
⊢ (g = w →
((f ⊆ g ∨ g ⊆ f)
↔ (w ⊆ f ∨ f ⊆ w))) |
44 | 43 | anbi2d 437 |
. . . . . . . . . 10
⊢ (g = w →
((Fun f ∧
(f ⊆ g ∨ g ⊆ f))
↔ (Fun f ∧ (w ⊆
f ∨
f ⊆ w)))) |
45 | | funeq 4864 |
. . . . . . . . . . 11
⊢ (f = v →
(Fun f ↔ Fun v)) |
46 | | sseq2 2961 |
. . . . . . . . . . . 12
⊢ (f = v →
(w ⊆ f ↔ w
⊆ v)) |
47 | | sseq1 2960 |
. . . . . . . . . . . 12
⊢ (f = v →
(f ⊆ w ↔ v
⊆ w)) |
48 | 46, 47 | orbi12d 706 |
. . . . . . . . . . 11
⊢ (f = v →
((w ⊆ f ∨ f ⊆ w)
↔ (w ⊆ v ∨ v ⊆ w))) |
49 | 45, 48 | anbi12d 442 |
. . . . . . . . . 10
⊢ (f = v →
((Fun f ∧
(w ⊆ f ∨ f ⊆ w))
↔ (Fun v ∧ (w ⊆
v ∨
v ⊆ w)))) |
50 | 44, 49 | cbvral2v 2535 |
. . . . . . . . 9
⊢ (∀g ∈ A ∀f ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f))
↔ ∀w ∈ A ∀v ∈ A (Fun v ∧ (w ⊆
v ∨
v ⊆ w))) |
51 | 38, 50 | bitri 173 |
. . . . . . . 8
⊢ (∀f ∈ A ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f))
↔ ∀w ∈ A ∀v ∈ A (Fun v ∧ (w ⊆
v ∨
v ⊆ w))) |
52 | 37, 51 | anbi12i 433 |
. . . . . . 7
⊢ ((∀f ∈ A ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f))
∧ ∀f ∈ A ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f)))
↔ (∀w ∈ A ∀v ∈ A (Fun w ∧ (w ⊆
v ∨
v ⊆ w)) ∧ ∀w ∈ A ∀v ∈ A (Fun
v ∧
(w ⊆ v ∨ v ⊆ w)))) |
53 | | anidm 376 |
. . . . . . 7
⊢ ((∀f ∈ A ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f))
∧ ∀f ∈ A ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f)))
↔ ∀f ∈ A ∀g ∈ A (Fun f ∧ (f ⊆
g ∨
g ⊆ f))) |
54 | | anandir 525 |
. . . . . . . . 9
⊢ (((Fun
w ∧ Fun
v) ∧
(w ⊆ v ∨ v ⊆ w))
↔ ((Fun w ∧ (w ⊆
v ∨
v ⊆ w)) ∧ (Fun v ∧ (w ⊆ v
∨ v
⊆ w)))) |
55 | 54 | 2ralbii 2326 |
. . . . . . . 8
⊢ (∀w ∈ A ∀v ∈ A ((Fun
w ∧ Fun
v) ∧
(w ⊆ v ∨ v ⊆ w))
↔ ∀w ∈ A ∀v ∈ A ((Fun w ∧ (w ⊆
v ∨
v ⊆ w)) ∧ (Fun v ∧ (w ⊆ v
∨ v
⊆ w)))) |
56 | | r19.26-2 2436 |
. . . . . . . 8
⊢ (∀w ∈ A ∀v ∈ A ((Fun
w ∧
(w ⊆ v ∨ v ⊆ w))
∧ (Fun v
∧ (w
⊆ v
∨ v ⊆ w))) ↔ (∀w ∈ A ∀v ∈ A (Fun
w ∧
(w ⊆ v ∨ v ⊆ w))
∧ ∀w ∈ A ∀v ∈ A (Fun
v ∧
(w ⊆ v ∨ v ⊆ w)))) |
57 | 55, 56 | bitr2i 174 |
. . . . . . 7
⊢ ((∀w ∈ A ∀v ∈ A (Fun
w ∧
(w ⊆ v ∨ v ⊆ w))
∧ ∀w ∈ A ∀v ∈ A (Fun
v ∧
(w ⊆ v ∨ v ⊆ w)))
↔ ∀w ∈ A ∀v ∈ A ((Fun w ∧ Fun v) ∧ (w ⊆
v ∨
v ⊆ w))) |
58 | 52, 53, 57 | 3bitr3i 199 |
. . . . . 6
⊢ (∀f ∈ A ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f))
↔ ∀w ∈ A ∀v ∈ A ((Fun w ∧ Fun v) ∧ (w ⊆
v ∨
v ⊆ w))) |
59 | | eluni 3574 |
. . . . . . . . . 10
⊢
(〈x, y〉 ∈ ∪ A ↔ ∃w(〈x,
y〉 ∈
w ∧
w ∈
A)) |
60 | | eluni 3574 |
. . . . . . . . . 10
⊢
(〈x, z〉 ∈ ∪ A ↔ ∃v(〈x,
z〉 ∈
v ∧
v ∈
A)) |
61 | 59, 60 | anbi12i 433 |
. . . . . . . . 9
⊢
((〈x, y〉 ∈ ∪ A ∧ 〈x,
z〉 ∈
∪ A) ↔
(∃w(〈x,
y〉 ∈
w ∧
w ∈
A) ∧ ∃v(〈x,
z〉 ∈
v ∧
v ∈
A))) |
62 | | eeanv 1804 |
. . . . . . . . 9
⊢ (∃w∃v((〈x,
y〉 ∈
w ∧
w ∈
A) ∧
(〈x, z〉 ∈ v ∧ v ∈ A)) ↔ (∃w(〈x,
y〉 ∈
w ∧
w ∈
A) ∧ ∃v(〈x,
z〉 ∈
v ∧
v ∈
A))) |
63 | | an4 520 |
. . . . . . . . . . 11
⊢
(((〈x, y〉 ∈ w ∧ w ∈ A) ∧
(〈x, z〉 ∈ v ∧ v ∈ A)) ↔ ((〈x, y〉 ∈ w ∧ 〈x,
z〉 ∈
v) ∧
(w ∈
A ∧
v ∈
A))) |
64 | | ancom 253 |
. . . . . . . . . . 11
⊢
(((〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v) ∧ (w ∈ A ∧ v ∈ A)) ↔
((w ∈
A ∧
v ∈
A) ∧
(〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v))) |
65 | 63, 64 | bitri 173 |
. . . . . . . . . 10
⊢
(((〈x, y〉 ∈ w ∧ w ∈ A) ∧
(〈x, z〉 ∈ v ∧ v ∈ A)) ↔ ((w
∈ A ∧ v ∈ A) ∧ (〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ v))) |
66 | 65 | 2exbii 1494 |
. . . . . . . . 9
⊢ (∃w∃v((〈x,
y〉 ∈
w ∧
w ∈
A) ∧
(〈x, z〉 ∈ v ∧ v ∈ A)) ↔ ∃w∃v((w ∈ A ∧ v ∈ A) ∧
(〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v))) |
67 | 61, 62, 66 | 3bitr2i 197 |
. . . . . . . 8
⊢
((〈x, y〉 ∈ ∪ A ∧ 〈x,
z〉 ∈
∪ A) ↔
∃w∃v((w ∈ A ∧ v ∈ A) ∧
(〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v))) |
68 | 67 | imbi1i 227 |
. . . . . . 7
⊢
(((〈x, y〉 ∈ ∪ A ∧ 〈x,
z〉 ∈
∪ A) →
y = z)
↔ (∃w∃v((w ∈ A ∧ v ∈ A) ∧ (〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ v)) → y =
z)) |
69 | | 19.23v 1760 |
. . . . . . 7
⊢ (∀w(∃v((w ∈ A ∧ v ∈ A) ∧
(〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v)) →
y = z)
↔ (∃w∃v((w ∈ A ∧ v ∈ A) ∧ (〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ v)) → y =
z)) |
70 | | r2al 2337 |
. . . . . . . 8
⊢ (∀w ∈ A ∀v ∈ A
((〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v) →
y = z)
↔ ∀w∀v((w ∈ A ∧ v ∈ A) →
((〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v) →
y = z))) |
71 | | impexp 250 |
. . . . . . . . 9
⊢
((((w ∈ A ∧ v ∈ A) ∧ (〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ v)) → y =
z) ↔ ((w ∈ A ∧ v ∈ A) → ((〈x, y〉 ∈ w ∧ 〈x,
z〉 ∈
v) → y = z))) |
72 | 71 | 2albii 1357 |
. . . . . . . 8
⊢ (∀w∀v(((w ∈ A ∧ v ∈ A) ∧
(〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v)) →
y = z)
↔ ∀w∀v((w ∈ A ∧ v ∈ A) →
((〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v) →
y = z))) |
73 | | 19.23v 1760 |
. . . . . . . . 9
⊢ (∀v(((w ∈ A ∧ v ∈ A) ∧
(〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v)) →
y = z)
↔ (∃v((w ∈ A ∧ v ∈ A) ∧ (〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ v)) → y =
z)) |
74 | 73 | albii 1356 |
. . . . . . . 8
⊢ (∀w∀v(((w ∈ A ∧ v ∈ A) ∧
(〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v)) →
y = z)
↔ ∀w(∃v((w ∈ A ∧ v ∈ A) ∧ (〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ v)) → y =
z)) |
75 | 70, 72, 74 | 3bitr2ri 198 |
. . . . . . 7
⊢ (∀w(∃v((w ∈ A ∧ v ∈ A) ∧
(〈x, y〉 ∈ w ∧ 〈x, z〉 ∈ v)) →
y = z)
↔ ∀w ∈ A ∀v ∈ A ((〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ v) → y =
z)) |
76 | 68, 69, 75 | 3bitr2i 197 |
. . . . . 6
⊢
(((〈x, y〉 ∈ ∪ A ∧ 〈x,
z〉 ∈
∪ A) →
y = z)
↔ ∀w ∈ A ∀v ∈ A ((〈x,
y〉 ∈
w ∧
〈x, z〉 ∈ v) → y =
z)) |
77 | 27, 58, 76 | 3imtr4i 190 |
. . . . 5
⊢ (∀f ∈ A ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f))
→ ((〈x, y〉 ∈ ∪ A ∧ 〈x,
z〉 ∈
∪ A) →
y = z)) |
78 | 77 | alrimiv 1751 |
. . . 4
⊢ (∀f ∈ A ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f))
→ ∀z((〈x,
y〉 ∈
∪ A ∧ 〈x,
z〉 ∈
∪ A) →
y = z)) |
79 | 78 | alrimivv 1752 |
. . 3
⊢ (∀f ∈ A ∀g ∈ A (Fun
f ∧
(f ⊆ g ∨ g ⊆ f))
→ ∀x∀y∀z((〈x,
y〉 ∈
∪ A ∧ 〈x,
z〉 ∈
∪ A) →
y = z)) |
80 | 7, 79 | syl 14 |
. 2
⊢ (∀f ∈ A (Fun
f ∧ ∀g ∈ A (f ⊆ g
∨ g
⊆ f)) → ∀x∀y∀z((〈x,
y〉 ∈
∪ A ∧ 〈x,
z〉 ∈
∪ A) →
y = z)) |
81 | | dffun4 4856 |
. 2
⊢ (Fun
∪ A ↔ (Rel
∪ A ∧ ∀x∀y∀z((〈x,
y〉 ∈
∪ A ∧ 〈x,
z〉 ∈
∪ A) →
y = z))) |
82 | 5, 80, 81 | sylanbrc 394 |
1
⊢ (∀f ∈ A (Fun
f ∧ ∀g ∈ A (f ⊆ g
∨ g
⊆ f)) → Fun ∪ A) |