This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 )