Step | Hyp | Ref
| Expression |
1 | | ssel 3893 |
. . . . . . . . . . 11
⊢ (𝑧 ⊆ 𝐴 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝐴)) |
2 | | ssel 3893 |
. . . . . . . . . . 11
⊢ (𝑧 ⊆ 𝐴 → (𝑦 ∈ 𝑧 → 𝑦 ∈ 𝐴)) |
3 | 1, 2 | anim12d 612 |
. . . . . . . . . 10
⊢ (𝑧 ⊆ 𝐴 → ((𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑧) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴))) |
4 | | brinxp 5627 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦𝑅𝑥 ↔ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
5 | 4 | ancoms 462 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑦𝑅𝑥 ↔ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
6 | 3, 5 | syl6 35 |
. . . . . . . . 9
⊢ (𝑧 ⊆ 𝐴 → ((𝑥 ∈ 𝑧 ∧ 𝑦 ∈ 𝑧) → (𝑦𝑅𝑥 ↔ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥))) |
7 | 6 | impl 459 |
. . . . . . . 8
⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑧) ∧ 𝑦 ∈ 𝑧) → (𝑦𝑅𝑥 ↔ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
8 | 7 | notbid 321 |
. . . . . . 7
⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑧) ∧ 𝑦 ∈ 𝑧) → (¬ 𝑦𝑅𝑥 ↔ ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
9 | 8 | ralbidva 3117 |
. . . . . 6
⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑥 ∈ 𝑧) → (∀𝑦 ∈ 𝑧 ¬ 𝑦𝑅𝑥 ↔ ∀𝑦 ∈ 𝑧 ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
10 | 9 | rexbidva 3215 |
. . . . 5
⊢ (𝑧 ⊆ 𝐴 → (∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 ¬ 𝑦𝑅𝑥 ↔ ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
11 | 10 | adantr 484 |
. . . 4
⊢ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → (∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 ¬ 𝑦𝑅𝑥 ↔ ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
12 | 11 | pm5.74i 274 |
. . 3
⊢ (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 ¬ 𝑦𝑅𝑥) ↔ ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
13 | 12 | albii 1827 |
. 2
⊢
(∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 ¬ 𝑦𝑅𝑥) ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
14 | | df-fr 5509 |
. 2
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 ¬ 𝑦𝑅𝑥)) |
15 | | df-fr 5509 |
. 2
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) Fr 𝐴 ↔ ∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅) → ∃𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 ¬ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑥)) |
16 | 13, 14, 15 | 3bitr4i 306 |
1
⊢ (𝑅 Fr 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) Fr 𝐴) |