| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢ ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)} = ∪ ∩ {𝑎
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑎)} |
| 2 | 1 | oeeulem 8639 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (∪ ∩ {𝑎
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑎)} ∈ On ∧ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 ↑o suc ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}))) |
| 3 | 2 | simp1d 1143 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∪ ∩ {𝑎
∈ On ∣ 𝐵 ∈
(𝐴 ↑o 𝑎)} ∈ On) |
| 4 | | fvexd 6921 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵))) ∈ V) |
| 5 | | fvexd 6921 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → (2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵))) ∈ V) |
| 6 | | eqid 2737 |
. . . 4
⊢
(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵)) = (℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵)) |
| 7 | | eqid 2737 |
. . . 4
⊢
(1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵))) = (1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑o ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑o 𝑎)}) ·o 𝑏) +o 𝑐) = 𝐵))) |
| 8 | | eqid 2737 |
. . . 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 8640 |
. . 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 5518 |
. 2
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∃!𝑤∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵))) |
| 11 | | df-3an 1089 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥))) |
| 12 | 11 | biancomi 462 |
. . . . . . . . . 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 645 |
. . . . . . . 8
⊢ ((𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑧 ∈ (𝐴 ↑o 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o))) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ ((𝑧 ∈ (𝐴 ↑o 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o))) ∧ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵))) |
| 16 | | anass 468 |
. . . . . . . 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 1848 |
. . . . . 6
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ ∃𝑧(𝑧 ∈ (𝐴 ↑o 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)))) |
| 19 | | df-rex 3071 |
. . . . . 6
⊢
(∃𝑧 ∈
(𝐴 ↑o 𝑥)((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ ∃𝑧(𝑧 ∈ (𝐴 ↑o 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)))) |
| 20 | | r19.42v 3191 |
. . . . . 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 1849 |
. . . 4
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o) ∧ 𝑧 ∈ (𝐴 ↑o 𝑥)) ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ ∃𝑧 ∈ (𝐴 ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵))) |
| 23 | | r2ex 3196 |
. . . 4
⊢
(∃𝑥 ∈ On
∃𝑦 ∈ (𝐴 ∖
1o)∃𝑧
∈ (𝐴
↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1o)) ∧ ∃𝑧 ∈ (𝐴 ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵))) |
| 24 | 22, 23 | bitr4i 278 |
. . 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 218 |
1
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ (On ∖ 1o)) → ∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (𝐴 ∖ 1o)∃𝑧 ∈ (𝐴 ↑o 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑o 𝑥) ·o 𝑦) +o 𝑧) = 𝐵)) |