Step |
Hyp |
Ref |
Expression |
1 |
|
iunfo.1 |
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) |
2 |
|
iundomg.2 |
⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↑m 𝐵 ) ∈ AC 𝐴 ) |
3 |
|
iundomg.3 |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ≼ 𝐶 ) |
4 |
|
iundomg.4 |
⊢ ( 𝜑 → ( 𝐴 × 𝐶 ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 ) |
5 |
1 2 3
|
iundom2g |
⊢ ( 𝜑 → 𝑇 ≼ ( 𝐴 × 𝐶 ) ) |
6 |
|
acndom2 |
⊢ ( 𝑇 ≼ ( 𝐴 × 𝐶 ) → ( ( 𝐴 × 𝐶 ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑇 ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 ) ) |
7 |
5 4 6
|
sylc |
⊢ ( 𝜑 → 𝑇 ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 ) |
8 |
1
|
iunfo |
⊢ ( 2nd ↾ 𝑇 ) : 𝑇 –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 |
9 |
|
fodomacn |
⊢ ( 𝑇 ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 → ( ( 2nd ↾ 𝑇 ) : 𝑇 –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ 𝑇 ) ) |
10 |
7 8 9
|
mpisyl |
⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ 𝑇 ) |
11 |
|
domtr |
⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ≼ 𝑇 ∧ 𝑇 ≼ ( 𝐴 × 𝐶 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ( 𝐴 × 𝐶 ) ) |
12 |
10 5 11
|
syl2anc |
⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ( 𝐴 × 𝐶 ) ) |