Theorem wdom2d2

Description: Deduction for weak dominance by a Cartesian product.MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015)

	Ref	Expression
Hypotheses	wdom2d2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	wdom2d2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	wdom2d2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
	wdom2d2.o	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = 𝑋 )
Assertion	wdom2d2	⊢ ( 𝜑 → 𝐴 ≼* ( 𝐵 × 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		wdom2d2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		wdom2d2.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		wdom2d2.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
4		wdom2d2.o	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = 𝑋 )
5	2 3	xpexd	⊢ ( 𝜑 → ( 𝐵 × 𝐶 ) ∈ V )
6		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ ( 1st ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑧 ⦌ 𝑋
7	6	nfeq2	⊢ Ⅎ 𝑦 𝑥 = ⦋ ( 1st ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑧 ⦌ 𝑋
8		nfcv	⊢ Ⅎ 𝑧 ( 1st ‘ 𝑤 )
9		nfcsb1v	⊢ Ⅎ 𝑧 ⦋ ( 2nd ‘ 𝑤 ) / 𝑧 ⦌ 𝑋
10	8 9	nfcsbw	⊢ Ⅎ 𝑧 ⦋ ( 1st ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑧 ⦌ 𝑋
11	10	nfeq2	⊢ Ⅎ 𝑧 𝑥 = ⦋ ( 1st ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑧 ⦌ 𝑋
12		nfv	⊢ Ⅎ 𝑤 𝑥 = 𝑋
13		csbopeq1a	⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ⦋ ( 1st ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑧 ⦌ 𝑋 = 𝑋 )
14	13	eqeq2d	⊢ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 = ⦋ ( 1st ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑧 ⦌ 𝑋 ↔ 𝑥 = 𝑋 ) )
15	7 11 12 14	rexxpf	⊢ ( ∃ 𝑤 ∈ ( 𝐵 × 𝐶 ) 𝑥 = ⦋ ( 1st ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑧 ⦌ 𝑋 ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑥 = 𝑋 )
16	4 15	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑤 ∈ ( 𝐵 × 𝐶 ) 𝑥 = ⦋ ( 1st ‘ 𝑤 ) / 𝑦 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑧 ⦌ 𝑋 )
17	1 5 16	wdom2d	⊢ ( 𝜑 → 𝐴 ≼* ( 𝐵 × 𝐶 ) )