Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . 5
⊢ ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)} = ∪ ∩ {𝑎
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑎)} |
2 | 1 | oeeulem 8419 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (∪ ∩ {𝑎
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑎)} ∈ On ∧ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 ↑o suc ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}))) |
3 | 2 | simp1d 1141 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∪ ∩ {𝑎
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑎)} ∈ On) |
4 | | fvexd 6781 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵))) ∈ V) |
5 | | fvexd 6781 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵))) ∈ V) |
6 | | eqid 2738 |
. . . 4
⊢
(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵)) = (℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵)) |
7 | | eqid 2738 |
. . . 4
⊢
(1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵))) = (1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵))) |
8 | | eqid 2738 |
. . . 4
⊢
(2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵))) = (2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵))) |
9 | 1, 6, 7, 8 | oeeui 8420 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵) ↔ (𝑥 = ∪ ∩ {𝑎
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑎)} ∧ 𝑦 = (1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵))) ∧ 𝑧 = (2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵)))))) |
10 | 3, 4, 5, 9 | euotd 5425 |
. 2
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∃!𝑤∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵))) |
11 | | df-3an 1088 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥))) |
12 | 11 | biancomi 463 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ↔ (𝑧 ∈ (𝐴 ↑o 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)))) |
13 | 12 | anbi1i 624 |
. . . . . . . . 9
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵) ↔ ((𝑧 ∈ (𝐴 ↑o 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o))) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) |
14 | 13 | anbi2i 623 |
. . . . . . . 8
⊢ ((𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑧 ∈ (𝐴 ↑o 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o))) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵))) |
15 | | an12 642 |
. . . . . . . 8
⊢ ((𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑧 ∈ (𝐴 ↑o 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o))) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ ((𝑧 ∈ (𝐴 ↑o 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o))) ∧ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵))) |
16 | | anass 469 |
. . . . . . . 8
⊢ (((𝑧 ∈ (𝐴 ↑o 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o))) ∧ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ (𝑧 ∈ (𝐴 ↑o 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)))) |
17 | 14, 15, 16 | 3bitri 297 |
. . . . . . 7
⊢ ((𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ (𝑧 ∈ (𝐴 ↑o 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)))) |
18 | 17 | exbii 1850 |
. . . . . 6
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ ∃𝑧(𝑧 ∈ (𝐴 ↑o 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)))) |
19 | | df-rex 3070 |
. . . . . 6
⊢
(∃𝑧 ∈
(𝐴 ↑o 𝑥)((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ ∃𝑧(𝑧 ∈ (𝐴 ↑o 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)))) |
20 | | r19.42v 3277 |
. . . . . 6
⊢
(∃𝑧 ∈
(𝐴 ↑o 𝑥)((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ ∃𝑧 ∈ (𝐴 ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵))) |
21 | 18, 19, 20 | 3bitr2i 299 |
. . . . 5
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ ∃𝑧 ∈ (𝐴 ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵))) |
22 | 21 | 2exbii 1851 |
. . . 4
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ ∃𝑧 ∈ (𝐴 ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵))) |
23 | | r2ex 3230 |
. . . 4
⊢
(∃𝑥 ∈ On
∃𝑦 ∈ (𝐴 ∖
1o)∃𝑧
∈ (𝐴
↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ ∃𝑧 ∈ (𝐴 ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵))) |
24 | 22, 23 | bitr4i 277 |
. . 3
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ ∃𝑥 ∈ On ∃𝑦 ∈ (𝐴 ∖ 1o)∃𝑧 ∈ (𝐴 ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) |
25 | 24 | eubii 2585 |
. 2
⊢
(∃!𝑤∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ ∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (𝐴 ∖ 1o)∃𝑧 ∈ (𝐴 ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) |
26 | 10, 25 | sylib 217 |
1
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (𝐴 ∖ 1o)∃𝑧 ∈ (𝐴 ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) |