Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . 6
⊢ ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} = ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} |
2 | 1 | oeeulem 7568 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ (∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} ∈ On ∧ (𝐴 ↑𝑜
∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ⊆ 𝐵 ∧ 𝐵 ∈ (𝐴 ↑𝑜 suc ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}))) |
3 | 2 | simp1d 1066 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} ∈ On) |
4 | | elex 3185 |
. . . 4
⊢ (∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} ∈ On → ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} ∈ V) |
5 | 3, 4 | syl 17 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)} ∈ V) |
6 | | fvex 6113 |
. . . 4
⊢
(1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) ∈ V |
7 | 6 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ (1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) ∈ V) |
8 | | fvex 6113 |
. . . 4
⊢
(2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ (2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) ∈ V) |
10 | | eqid 2610 |
. . . 4
⊢
(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵)) = (℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵)) |
11 | | eqid 2610 |
. . . 4
⊢
(1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) = (1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) |
12 | | eqid 2610 |
. . . 4
⊢
(2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) = (2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) |
13 | 1, 10, 11, 12 | oeeui 7569 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ (((𝑥 ∈ On ∧
𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵) ↔ (𝑥 = ∪ ∩ {𝑎
∈ On ∣ 𝐵 ∈
(𝐴
↑𝑜 𝑎)} ∧ 𝑦 = (1st ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵))) ∧ 𝑧 = (2nd ‘(℩𝑑∃𝑏 ∈ On ∃𝑐 ∈ (𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)})(𝑑 = 〈𝑏, 𝑐〉 ∧ (((𝐴 ↑𝑜 ∪ ∩ {𝑎 ∈ On ∣ 𝐵 ∈ (𝐴 ↑𝑜 𝑎)}) ·𝑜
𝑏) +𝑜
𝑐) = 𝐵)))))) |
14 | 5, 7, 9, 13 | euotd 4900 |
. 2
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ ∃!𝑤∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵))) |
15 | | df-3an 1033 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥))) |
16 | | ancom 465 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ↔ (𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖
1𝑜)))) |
17 | 15, 16 | bitri 263 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ↔ (𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖
1𝑜)))) |
18 | 17 | anbi1i 727 |
. . . . . . . . 9
⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵) ↔ ((𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜))) ∧
(((𝐴
↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵)) |
19 | 18 | anbi2i 726 |
. . . . . . . 8
⊢ ((𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ (𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜))) ∧
(((𝐴
↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵))) |
20 | | an12 834 |
. . . . . . . 8
⊢ ((𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜))) ∧
(((𝐴
↑𝑜 𝑥) ·𝑜 𝑦) +𝑜 𝑧) = 𝐵)) ↔ ((𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜))) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵))) |
21 | | anass 679 |
. . . . . . . 8
⊢ (((𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ (𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜))) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ (𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)))) |
22 | 19, 20, 21 | 3bitri 285 |
. . . . . . 7
⊢ ((𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ (𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)))) |
23 | 22 | exbii 1764 |
. . . . . 6
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ∃𝑧(𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)))) |
24 | | df-rex 2902 |
. . . . . 6
⊢
(∃𝑧 ∈
(𝐴
↑𝑜 𝑥)((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ∃𝑧(𝑧 ∈ (𝐴 ↑𝑜 𝑥) ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)))) |
25 | | r19.42v 3073 |
. . . . . 6
⊢
(∃𝑧 ∈
(𝐴
↑𝑜 𝑥)((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
∃𝑧 ∈ (𝐴 ↑𝑜
𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵))) |
26 | 23, 24, 25 | 3bitr2i 287 |
. . . . 5
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
∃𝑧 ∈ (𝐴 ↑𝑜
𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵))) |
27 | 26 | 2exbii 1765 |
. . . 4
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
∃𝑧 ∈ (𝐴 ↑𝑜
𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵))) |
28 | | r2ex 3043 |
. . . 4
⊢
(∃𝑥 ∈ On
∃𝑦 ∈ (𝐴 ∖
1𝑜)∃𝑧 ∈ (𝐴 ↑𝑜 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵) ↔ ∃𝑥∃𝑦((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜)) ∧
∃𝑧 ∈ (𝐴 ↑𝑜
𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵))) |
29 | 27, 28 | bitr4i 266 |
. . 3
⊢
(∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ∃𝑥 ∈ On ∃𝑦 ∈ (𝐴 ∖ 1𝑜)∃𝑧 ∈ (𝐴 ↑𝑜 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) |
30 | 29 | eubii 2480 |
. 2
⊢
(∃!𝑤∃𝑥∃𝑦∃𝑧(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ ((𝑥 ∈ On ∧ 𝑦 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑧 ∈ (𝐴 ↑𝑜 𝑥)) ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) ↔ ∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (𝐴 ∖ 1𝑜)∃𝑧 ∈ (𝐴 ↑𝑜 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) |
31 | 14, 30 | sylib 207 |
1
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ (On ∖ 1𝑜))
→ ∃!𝑤∃𝑥 ∈ On ∃𝑦 ∈ (𝐴 ∖ 1𝑜)∃𝑧 ∈ (𝐴 ↑𝑜 𝑥)(𝑤 = 〈𝑥, 𝑦, 𝑧〉 ∧ (((𝐴 ↑𝑜 𝑥) ·𝑜
𝑦) +𝑜
𝑧) = 𝐵)) |