This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 dfss2 ⊢ ( 𝑥 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝑥 ∩ ( 𝐵 ∪ 𝐶 ) ) = 𝑥 )
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 ⊢ ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵 ∪ 𝐶 ) → ( 𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶 ) )