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 ( ( 𝐴 × 𝐴 ) ≼ ( 𝐵𝐶 ) → ( 𝐴* 𝐵𝐴𝐶 ) )