Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . 6
⊢ ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} = ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} |
2 | 1 | oeeulem 7681 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ (∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} ∈ On ∧ (𝐴 ↑𝑜
∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 ↑𝑜 suc ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}))) |
3 | 2 | simp1d 1073 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} ∈ On) |
4 | | elex 3212 |
. . . 4
⊢ (∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} ∈ On → ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} ∈ V) |
5 | 3, 4 | syl 17 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} ∈ V) |
6 | | fvexd 6203 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ (1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) ∈ V) |
7 | | fvexd 6203 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ (2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) ∈ V) |
8 | | eqid 2622 |
. . . 4
⊢
(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵)) = (℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵)) |
9 | | eqid 2622 |
. . . 4
⊢
(1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) = (1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) |
10 | | eqid 2622 |
. . . 4
⊢
(2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) = (2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) |
11 | 1, 8, 9, 10 | oeeui 7682 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ (((𝑥 ∈ On ∧
𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵) ↔ (𝑥 = ∪ ∩ {𝑎
∈ On ∣ 𝐵 ∈
(𝐴
↑𝑜 𝑎)} ∧ 𝑦 = (1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) ∧ 𝑧 = (2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵)))))) |
12 | 5, 6, 7, 11 | euotd 4975 |
. 2
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ ∃!𝑤∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵))) |
13 | | df-3an 1039 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥))) |
14 | | ancom 466 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ↔ (𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖
1𝑜)))) |
15 | 13, 14 | bitri 264 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ↔ (𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖
1𝑜)))) |
16 | 15 | anbi1i 731 |
. . . . . . . . 9
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵) ↔ ((𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜))) ∧
(((𝐴
↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵)) |
17 | 16 | anbi2i 730 |
. . . . . . . 8
⊢ ((𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜))) ∧
(((𝐴
↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵))) |
18 | | an12 838 |
. . . . . . . 8
⊢ ((𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜))) ∧
(((𝐴
↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵)) ↔ ((𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜))) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵))) |
19 | | anass 681 |
. . . . . . . 8
⊢ (((𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜))) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ (𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)))) |
20 | 17, 18, 19 | 3bitri 286 |
. . . . . . 7
⊢ ((𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ (𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)))) |
21 | 20 | exbii 1774 |
. . . . . 6
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ∃𝑧(𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)))) |
22 | | df-rex 2918 |
. . . . . 6
⊢
(∃𝑧 ∈
(𝐴
↑𝑜 𝑥)((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ∃𝑧(𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)))) |
23 | | r19.42v 3092 |
. . . . . 6
⊢
(∃𝑧 ∈
(𝐴
↑𝑜 𝑥)((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
∃𝑧 ∈ (𝐴 ↑𝑜
𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵))) |
24 | 21, 22, 23 | 3bitr2i 288 |
. . . . 5
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
∃𝑧 ∈ (𝐴 ↑𝑜
𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵))) |
25 | 24 | 2exbii 1775 |
. . . 4
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
∃𝑧 ∈ (𝐴 ↑𝑜
𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵))) |
26 | | r2ex 3061 |
. . . 4
⊢
(∃𝑥 ∈ On
∃𝑦 ∈ (𝐴 ∖
1𝑜)∃𝑧 ∈ (𝐴 ↑𝑜 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
∃𝑧 ∈ (𝐴 ↑𝑜
𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵))) |
27 | 25, 26 | bitr4i 267 |
. . 3
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ∃𝑥 ∈ On ∃𝑦 ∈ (𝐴 ∖ 1𝑜)∃𝑧 ∈ (𝐴 ↑𝑜 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) |
28 | 27 | eubii 2492 |
. 2
⊢
(∃!𝑤∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (𝐴 ∖ 1𝑜)∃𝑧 ∈ (𝐴 ↑𝑜 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) |
29 | 12, 28 | sylib 208 |
1
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ ∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (𝐴 ∖ 1𝑜)∃𝑧 ∈ (𝐴 ↑𝑜 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) |