Metamath Proof Explorer

Theorem disjen

Description: A stronger form of pwuninel . We can use pwuninel , 2pwuninel to create one or two sets disjoint from a given set A , but here we show that in fact such constructions exist for arbitrarily large disjoint extensions, which is to say that for any set B we can construct a set x that is equinumerous to it and disjoint from A . (Contributed by Mario Carneiro, 7-Feb-2015)

Ref Expression
Assertion disjen ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∩ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) = ∅ ∧ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ≈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 1st2nd2 ⊢ ( 𝑥 ∈ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) → 𝑥 = ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
2 1 ad2antll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) ) → 𝑥 = ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ )
3 simprl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) ) → 𝑥 ∈ 𝐴 )
4 2 3 eqeltrrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) ) → ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ∈ 𝐴 )
5 fvex ⊢ ( 1st ‘ 𝑥 ) ∈ V
6 fvex ⊢ ( 2nd ‘ 𝑥 ) ∈ V
7 5 6 opelrn ⊢ ( ⟨ ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) ⟩ ∈ 𝐴 → ( 2nd ‘ 𝑥 ) ∈ ran 𝐴 )
8 4 7 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( 2nd ‘ 𝑥 ) ∈ ran 𝐴 )
9 pwuninel ⊢ ¬ 𝒫 ∪ ran 𝐴 ∈ ran 𝐴
10 xp2nd ⊢ ( 𝑥 ∈ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) → ( 2nd ‘ 𝑥 ) ∈ { 𝒫 ∪ ran 𝐴 } )
11 10 ad2antll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( 2nd ‘ 𝑥 ) ∈ { 𝒫 ∪ ran 𝐴 } )
12 elsni ⊢ ( ( 2nd ‘ 𝑥 ) ∈ { 𝒫 ∪ ran 𝐴 } → ( 2nd ‘ 𝑥 ) = 𝒫 ∪ ran 𝐴 )
13 11 12 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( 2nd ‘ 𝑥 ) = 𝒫 ∪ ran 𝐴 )
14 13 eleq1d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( ( 2nd ‘ 𝑥 ) ∈ ran 𝐴 ↔ 𝒫 ∪ ran 𝐴 ∈ ran 𝐴 ) )
15 9 14 mtbiri ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) ) → ¬ ( 2nd ‘ 𝑥 ) ∈ ran 𝐴 )
16 8 15 pm2.65da ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) )
17 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) )
18 16 17 sylnibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ¬ 𝑥 ∈ ( 𝐴 ∩ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) )
19 18 eq0rdv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∩ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) = ∅ )
20 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 )
21 rnexg ⊢ ( 𝐴 ∈ 𝑉 → ran 𝐴 ∈ V )
22 21 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran 𝐴 ∈ V )
23 uniexg ⊢ ( ran 𝐴 ∈ V → ∪ ran 𝐴 ∈ V )
24 pwexg ⊢ ( ∪ ran 𝐴 ∈ V → 𝒫 ∪ ran 𝐴 ∈ V )
25 22 23 24 3syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ∪ ran 𝐴 ∈ V )
26 xpsneng ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝒫 ∪ ran 𝐴 ∈ V ) → ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ≈ 𝐵 )
27 20 25 26 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ≈ 𝐵 )
28 19 27 jca ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∩ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) = ∅ ∧ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ≈ 𝐵 ) )