Step | Hyp | Ref
| Expression |
1 | | nfv 1418 |
. . . . . . . . . . . . . 14
⊢
Ⅎv(f ∈ 𝑐 ∧
∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒)) |
2 | 1 | sb8eu 1910 |
. . . . . . . . . . . . 13
⊢ (∃!f(f ∈ 𝑐 ∧
∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒)) ↔ ∃!v[v / f](f ∈ 𝑐 ∧
∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒))) |
3 | | eleq12 2099 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((f = v ∧ 𝑐 = z)
→ (f ∈ 𝑐 ↔ v
∈ z)) |
4 | 3 | ancoms 255 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐 = z ∧ f = v) →
(f ∈
𝑐 ↔ v ∈ z)) |
5 | 4 | 3adant3 923 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = z ∧ f = v ∧ 𝑏
= y) → (f ∈ 𝑐 ↔ v ∈ z)) |
6 | | eleq12 2099 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑐 = z ∧ 𝑒 = u)
→ (𝑐 ∈ 𝑒 ↔ z
∈ u)) |
7 | 6 | 3ad2antl1 1065 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑐 = z ∧ f = v ∧ 𝑏
= y) ∧
𝑒 = u) → (𝑐 ∈ 𝑒 ↔ z ∈ u)) |
8 | | eleq12 2099 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((f = v ∧ 𝑒 = u)
→ (f ∈ 𝑒 ↔ v
∈ u)) |
9 | 8 | 3ad2antl2 1066 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑐 = z ∧ f = v ∧ 𝑏
= y) ∧
𝑒 = u) → (f
∈ 𝑒 ↔ v
∈ u)) |
10 | 7, 9 | anbi12d 442 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑐 = z ∧ f = v ∧ 𝑏
= y) ∧
𝑒 = u) → ((𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) ↔ (z ∈ u ∧ v ∈ u))) |
11 | | simpl3 908 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑐 = z ∧ f = v ∧ 𝑏
= y) ∧
𝑒 = u) → 𝑏 = y) |
12 | 10, 11 | cbvrexdva2 2532 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = z ∧ f = v ∧ 𝑏
= y) → (∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) ↔ ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
13 | 5, 12 | anbi12d 442 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = z ∧ f = v ∧ 𝑏
= y) → ((f ∈ 𝑐 ∧
∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒)) ↔ (v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u)))) |
14 | 13 | 3com23 1109 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = z ∧ 𝑏 = y
∧ f =
v) → ((f ∈ 𝑐 ∧
∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒)) ↔ (v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u)))) |
15 | 14 | 3expa 1103 |
. . . . . . . . . . . . . . 15
⊢ (((𝑐 = z ∧ 𝑏 = y)
∧ f =
v) → ((f ∈ 𝑐 ∧
∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒)) ↔ (v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u)))) |
16 | 15 | sbiedv 1669 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 = z ∧ 𝑏 = y)
→ ([v / f](f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒)) ↔ (v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u)))) |
17 | 16 | eubidv 1905 |
. . . . . . . . . . . . 13
⊢ ((𝑐 = z ∧ 𝑏 = y)
→ (∃!v[v / f](f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒)) ↔ ∃!v(v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u)))) |
18 | 2, 17 | syl5bb 181 |
. . . . . . . . . . . 12
⊢ ((𝑐 = z ∧ 𝑏 = y)
→ (∃!f(f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒)) ↔ ∃!v(v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u)))) |
19 | | df-reu 2307 |
. . . . . . . . . . . 12
⊢ (∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) ↔ ∃!f(f ∈ 𝑐 ∧
∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒))) |
20 | | df-reu 2307 |
. . . . . . . . . . . 12
⊢ (∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) ↔ ∃!v(v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
21 | 18, 19, 20 | 3bitr4g 212 |
. . . . . . . . . . 11
⊢ ((𝑐 = z ∧ 𝑏 = y)
→ (∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) ↔ ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
22 | 21 | adantr 261 |
. . . . . . . . . 10
⊢ (((𝑐 = z ∧ 𝑏 = y)
∧ 𝑑 = w)
→ (∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) ↔ ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
23 | | simpll 481 |
. . . . . . . . . 10
⊢ (((𝑐 = z ∧ 𝑏 = y)
∧ 𝑑 = w)
→ 𝑐 = z) |
24 | 22, 23 | cbvraldva2 2531 |
. . . . . . . . 9
⊢ ((𝑐 = z ∧ 𝑏 = y)
→ (∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) ↔ ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
25 | 24 | ancoms 255 |
. . . . . . . 8
⊢ ((𝑏 = y ∧ 𝑐 = z)
→ (∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) ↔ ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
26 | 25 | adantll 445 |
. . . . . . 7
⊢ (((𝑎 = x ∧ 𝑏 = y)
∧ 𝑐 = z)
→ (∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) ↔ ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
27 | | simpll 481 |
. . . . . . 7
⊢ (((𝑎 = x ∧ 𝑏 = y)
∧ 𝑐 = z)
→ 𝑎 = x) |
28 | 26, 27 | cbvraldva2 2531 |
. . . . . 6
⊢ ((𝑎 = x ∧ 𝑏 = y)
→ (∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) ↔ ∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
29 | 28 | cbvexdva 1801 |
. . . . 5
⊢ (𝑎 = x → (∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) ↔ ∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
30 | 29 | cbvalv 1791 |
. . . 4
⊢ (∀𝑎∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) ↔ ∀x∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)) |
31 | | acexmid.choice |
. . . 4
⊢ ∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) |
32 | 30, 31 | mpgbir 1339 |
. . 3
⊢ ∀𝑎∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) |
33 | 32 | spi 1426 |
. 2
⊢ ∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧
f ∈ 𝑒) |
34 | 33 | acexmidlemv 5453 |
1
⊢ (φ ∨ ¬
φ) |