Theorem frinxp

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

	Ref	Expression
Assertion	frinxp	⊢ ( 𝑅 Fr 𝐴 ↔ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) Fr 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssel	⊢ ( 𝑧 ⊆ 𝐴 → ( 𝑥 ∈ 𝑧 → 𝑥 ∈ 𝐴 ) )
2		ssel	⊢ ( 𝑧 ⊆ 𝐴 → ( 𝑦 ∈ 𝑧 → 𝑦 ∈ 𝐴 ) )
3	1 2	anim12d	⊢ ( 𝑧 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑧 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) )
4		brinxp	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
5	4	ancoms	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
6	3 5	syl6	⊢ ( 𝑧 ⊆ 𝐴 → ( ( 𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑧 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) ) )
7	6	impl	⊢ ( ( ( 𝑧 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑧 ) ∧ 𝑦 ∈ 𝑧 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
8	7	notbid	⊢ ( ( ( 𝑧 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑧 ) ∧ 𝑦 ∈ 𝑧 ) → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
9	8	ralbidva	⊢ ( ( 𝑧 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑧 ) → ( ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
10	9	rexbidva	⊢ ( 𝑧 ⊆ 𝐴 → ( ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
11	10	adantr	⊢ ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ( ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ↔ ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
12	11	pm5.74i	⊢ ( ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ) ↔ ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
13	12	albii	⊢ ( ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
14		df-fr	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 𝑅 𝑥 ) )
15		df-fr	⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) Fr 𝐴 ↔ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑧 ∀ 𝑦 ∈ 𝑧 ¬ 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
16	13 14 15	3bitr4i	⊢ ( 𝑅 Fr 𝐴 ↔ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) Fr 𝐴 )