Metamath Proof Explorer

Theorem unxpwdom

Description: If a Cartesian product is dominated by a union, then the base set is either weakly dominated by one factor of the union or dominated by the other. Extracted from Lemma 2.3 of KanamoriPincus p. 420. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion unxpwdom ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 reldom ⊢ Rel ≼
2 1 brrelex2i ⊢ ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) → ( 𝐵 ∪ 𝐶 ) ∈ V )
3 domeng ⊢ ( ( 𝐵 ∪ 𝐶 ) ∈ V → ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ↔ ∃ 𝑥 ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) )
4 2 3 syl ⊢ ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) → ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ↔ ∃ 𝑥 ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) )
5 4 ibi ⊢ ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) → ∃ 𝑥 ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) )
6 simprl ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( 𝐴 × 𝐴 ) ≈ 𝑥 )
7 indi ⊢ ( 𝑥 ∩ ( 𝐵 ∪ 𝐶 ) ) = ( ( 𝑥 ∩ 𝐵 ) ∪ ( 𝑥 ∩ 𝐶 ) )
8 simprr ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) )
9 df-ss ⊢ ( 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑥 ∩ ( 𝐵 ∪ 𝐶 ) ) = 𝑥 )
10 8 9 sylib ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( 𝑥 ∩ ( 𝐵 ∪ 𝐶 ) ) = 𝑥 )
11 7 10 eqtr3id ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( ( 𝑥 ∩ 𝐵 ) ∪ ( 𝑥 ∩ 𝐶 ) ) = 𝑥 )
12 6 11 breqtrrd ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( 𝐴 × 𝐴 ) ≈ ( ( 𝑥 ∩ 𝐵 ) ∪ ( 𝑥 ∩ 𝐶 ) ) )
13 unxpwdom2 ⊢ ( ( 𝐴 × 𝐴 ) ≈ ( ( 𝑥 ∩ 𝐵 ) ∪ ( 𝑥 ∩ 𝐶 ) ) → ( 𝐴 ≼* ( 𝑥 ∩ 𝐵 ) ∨ 𝐴 ≼ ( 𝑥 ∩ 𝐶 ) ) )
14 12 13 syl ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( 𝐴 ≼* ( 𝑥 ∩ 𝐵 ) ∨ 𝐴 ≼ ( 𝑥 ∩ 𝐶 ) ) )
15 ssun1 ⊢ 𝐵 ⊆ ( 𝐵 ∪ 𝐶 )
16 2 adantr ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( 𝐵 ∪ 𝐶 ) ∈ V )
17 ssexg ⊢ ( ( 𝐵 ⊆ ( 𝐵 ∪ 𝐶 ) ∧ ( 𝐵 ∪ 𝐶 ) ∈ V ) → 𝐵 ∈ V )
18 15 16 17 sylancr ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → 𝐵 ∈ V )
19 inss2 ⊢ ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵
20 ssdomg ⊢ ( 𝐵 ∈ V → ( ( 𝑥 ∩ 𝐵 ) ⊆ 𝐵 → ( 𝑥 ∩ 𝐵 ) ≼ 𝐵 ) )
21 18 19 20 mpisyl ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( 𝑥 ∩ 𝐵 ) ≼ 𝐵 )
22 domwdom ⊢ ( ( 𝑥 ∩ 𝐵 ) ≼ 𝐵 → ( 𝑥 ∩ 𝐵 ) ≼* 𝐵 )
23 21 22 syl ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( 𝑥 ∩ 𝐵 ) ≼* 𝐵 )
24 wdomtr ⊢ ( ( 𝐴 ≼* ( 𝑥 ∩ 𝐵 ) ∧ ( 𝑥 ∩ 𝐵 ) ≼* 𝐵 ) → 𝐴 ≼* 𝐵 )
25 24 expcom ⊢ ( ( 𝑥 ∩ 𝐵 ) ≼* 𝐵 → ( 𝐴 ≼* ( 𝑥 ∩ 𝐵 ) → 𝐴 ≼* 𝐵 ) )
26 23 25 syl ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( 𝐴 ≼* ( 𝑥 ∩ 𝐵 ) → 𝐴 ≼* 𝐵 ) )
27 ssun2 ⊢ 𝐶 ⊆ ( 𝐵 ∪ 𝐶 )
28 ssexg ⊢ ( ( 𝐶 ⊆ ( 𝐵 ∪ 𝐶 ) ∧ ( 𝐵 ∪ 𝐶 ) ∈ V ) → 𝐶 ∈ V )
29 27 16 28 sylancr ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → 𝐶 ∈ V )
30 inss2 ⊢ ( 𝑥 ∩ 𝐶 ) ⊆ 𝐶
31 ssdomg ⊢ ( 𝐶 ∈ V → ( ( 𝑥 ∩ 𝐶 ) ⊆ 𝐶 → ( 𝑥 ∩ 𝐶 ) ≼ 𝐶 ) )
32 29 30 31 mpisyl ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( 𝑥 ∩ 𝐶 ) ≼ 𝐶 )
33 domtr ⊢ ( ( 𝐴 ≼ ( 𝑥 ∩ 𝐶 ) ∧ ( 𝑥 ∩ 𝐶 ) ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
34 33 expcom ⊢ ( ( 𝑥 ∩ 𝐶 ) ≼ 𝐶 → ( 𝐴 ≼ ( 𝑥 ∩ 𝐶 ) → 𝐴 ≼ 𝐶 ) )
35 32 34 syl ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( 𝐴 ≼ ( 𝑥 ∩ 𝐶 ) → 𝐴 ≼ 𝐶 ) )
36 26 35 orim12d ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( ( 𝐴 ≼* ( 𝑥 ∩ 𝐵 ) ∨ 𝐴 ≼ ( 𝑥 ∩ 𝐶 ) ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) ) )
37 14 36 mpd ⊢ ( ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) ∧ ( ( 𝐴 × 𝐴 ) ≈ 𝑥 ∧ 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ) ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) )
38 5 37 exlimddv ⊢ ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) )