| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . 4
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → 𝐸 = (ω ↑o
𝐷)) | 
| 2 |  | omelon 9687 | . . . . 5
⊢ ω
∈ On | 
| 3 |  | simpl 482 | . . . . 5
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → 𝐷 ∈ On) | 
| 4 |  | oecl 8576 | . . . . 5
⊢ ((ω
∈ On ∧ 𝐷 ∈
On) → (ω ↑o 𝐷) ∈ On) | 
| 5 | 2, 3, 4 | sylancr 587 | . . . 4
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → (ω
↑o 𝐷)
∈ On) | 
| 6 | 1, 5 | eqeltrd 2840 | . . 3
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → 𝐸 ∈ On) | 
| 7 | 3, 2 | jctil 519 | . . . . . . . 8
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → (ω ∈
On ∧ 𝐷 ∈
On)) | 
| 8 |  | peano1 7911 | . . . . . . . 8
⊢ ∅
∈ ω | 
| 9 |  | oen0 8625 | . . . . . . . 8
⊢
(((ω ∈ On ∧ 𝐷 ∈ On) ∧ ∅ ∈ ω)
→ ∅ ∈ (ω ↑o 𝐷)) | 
| 10 | 7, 8, 9 | sylancl 586 | . . . . . . 7
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → ∅ ∈
(ω ↑o 𝐷)) | 
| 11 | 10, 1 | eleqtrrd 2843 | . . . . . 6
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → ∅ ∈
𝐸) | 
| 12 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑥 = ∅ → (𝑥 +o 𝐸) = (∅ +o 𝐸)) | 
| 13 | 12 | sseq2d 4015 | . . . . . . 7
⊢ (𝑥 = ∅ → (𝐸 ⊆ (𝑥 +o 𝐸) ↔ 𝐸 ⊆ (∅ +o 𝐸))) | 
| 14 | 13 | adantl 481 | . . . . . 6
⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) ∧ 𝑥 = ∅) → (𝐸 ⊆ (𝑥 +o 𝐸) ↔ 𝐸 ⊆ (∅ +o 𝐸))) | 
| 15 |  | oa0r 8577 | . . . . . . . 8
⊢ (𝐸 ∈ On → (∅
+o 𝐸) = 𝐸) | 
| 16 | 6, 15 | syl 17 | . . . . . . 7
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → (∅
+o 𝐸) = 𝐸) | 
| 17 |  | ssid 4005 | . . . . . . 7
⊢ (∅
+o 𝐸) ⊆
(∅ +o 𝐸) | 
| 18 | 16, 17 | eqsstrrdi 4028 | . . . . . 6
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → 𝐸 ⊆ (∅ +o
𝐸)) | 
| 19 | 11, 14, 18 | rspcedvd 3623 | . . . . 5
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → ∃𝑥 ∈ 𝐸 𝐸 ⊆ (𝑥 +o 𝐸)) | 
| 20 |  | ssiun 5045 | . . . . 5
⊢
(∃𝑥 ∈
𝐸 𝐸 ⊆ (𝑥 +o 𝐸) → 𝐸 ⊆ ∪
𝑥 ∈ 𝐸 (𝑥 +o 𝐸)) | 
| 21 | 19, 20 | syl 17 | . . . 4
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → 𝐸 ⊆ ∪ 𝑥 ∈ 𝐸 (𝑥 +o 𝐸)) | 
| 22 | 1 | eleq2d 2826 | . . . . . . . 8
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → (𝑥 ∈ 𝐸 ↔ 𝑥 ∈ (ω ↑o 𝐷))) | 
| 23 | 22 | biimpa 476 | . . . . . . 7
⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) ∧ 𝑥 ∈ 𝐸) → 𝑥 ∈ (ω ↑o 𝐷)) | 
| 24 | 6 | adantr 480 | . . . . . . 7
⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) ∧ 𝑥 ∈ 𝐸) → 𝐸 ∈ On) | 
| 25 | 1 | adantr 480 | . . . . . . . 8
⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) ∧ 𝑥 ∈ 𝐸) → 𝐸 = (ω ↑o 𝐷)) | 
| 26 |  | ssid 4005 | . . . . . . . 8
⊢ 𝐸 ⊆ 𝐸 | 
| 27 | 25, 26 | eqsstrrdi 4028 | . . . . . . 7
⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) ∧ 𝑥 ∈ 𝐸) → (ω ↑o 𝐷) ⊆ 𝐸) | 
| 28 |  | oaabs2 8688 | . . . . . . 7
⊢ (((𝑥 ∈ (ω
↑o 𝐷) ∧
𝐸 ∈ On) ∧ (ω
↑o 𝐷)
⊆ 𝐸) → (𝑥 +o 𝐸) = 𝐸) | 
| 29 | 23, 24, 27, 28 | syl21anc 837 | . . . . . 6
⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) ∧ 𝑥 ∈ 𝐸) → (𝑥 +o 𝐸) = 𝐸) | 
| 30 | 29, 26 | eqsstrdi 4027 | . . . . 5
⊢ (((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) ∧ 𝑥 ∈ 𝐸) → (𝑥 +o 𝐸) ⊆ 𝐸) | 
| 31 | 30 | iunssd 5049 | . . . 4
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → ∪ 𝑥 ∈ 𝐸 (𝑥 +o 𝐸) ⊆ 𝐸) | 
| 32 | 21, 31 | eqssd 4000 | . . 3
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → 𝐸 = ∪ 𝑥 ∈ 𝐸 (𝑥 +o 𝐸)) | 
| 33 | 6, 6, 32 | 3jca 1128 | . 2
⊢ ((𝐷 ∈ On ∧ 𝐸 = (ω ↑o
𝐷)) → (𝐸 ∈ On ∧ 𝐸 ∈ On ∧ 𝐸 = ∪ 𝑥 ∈ 𝐸 (𝑥 +o 𝐸))) | 
| 34 |  | ofoafg 43372 | . 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = (𝐴 ∩ 𝐵)) ∧ (𝐸 ∈ On ∧ 𝐸 ∈ On ∧ 𝐸 = ∪ 𝑥 ∈ 𝐸 (𝑥 +o 𝐸))) → ( ∘f
+o ↾ ((𝐸
↑m 𝐴)
× (𝐸
↑m 𝐵))):((𝐸 ↑m 𝐴) × (𝐸 ↑m 𝐵))⟶(𝐸 ↑m 𝐶)) | 
| 35 | 33, 34 | sylan2 593 | 1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 = (𝐴 ∩ 𝐵)) ∧ (𝐷 ∈ On ∧ 𝐸 = (ω ↑o 𝐷))) → ( ∘f
+o ↾ ((𝐸
↑m 𝐴)
× (𝐸
↑m 𝐵))):((𝐸 ↑m 𝐴) × (𝐸 ↑m 𝐵))⟶(𝐸 ↑m 𝐶)) |