Theorem poinxp

Description: Intersection of partial order with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014)

	Ref	Expression
Assertion	poinxp	⊢ ( 𝑅 Po 𝐴 ↔ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) Po 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		brinxp	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑥 ↔ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
2	1	anidms	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 𝑅 𝑥 ↔ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
3	2	ad2antrr	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑥 ↔ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
4	3	notbid	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( ¬ 𝑥 𝑅 𝑥 ↔ ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
5		brinxp	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ) )
6	5	adantr	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ) )
7		brinxp	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑧 ↔ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) )
8	7	adantll	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑧 ↔ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) )
9	6 8	anbi12d	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ↔ ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ) )
10		brinxp	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑧 ↔ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) )
11	10	adantlr	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑧 ↔ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) )
12	9 11	imbi12d	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ) )
13	4 12	anbi12d	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ) ) )
14	13	ralbidva	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ) ) )
15	14	ralbidva	⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ) ) )
16	15	ralbiia	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ) )
17		df-po	⊢ ( 𝑅 Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
18		df-po	⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) ) )
19	16 17 18	3bitr4i	⊢ ( 𝑅 Po 𝐴 ↔ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) Po 𝐴 )