Proof of Theorem 2elresin
Step | Hyp | Ref
| Expression |
1 | | fnop 5272 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) → 𝑥 ∈ 𝐴) |
2 | | fnop 5272 |
. . . . . . . 8
⊢ ((𝐺 Fn 𝐵 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) → 𝑥 ∈ 𝐵) |
3 | 1, 2 | anim12i 336 |
. . . . . . 7
⊢ (((𝐹 Fn 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ∧ (𝐺 Fn 𝐵 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
4 | 3 | an4s 578 |
. . . . . 6
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
5 | | elin 3290 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
6 | 4, 5 | sylibr 133 |
. . . . 5
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) → 𝑥 ∈ (𝐴 ∩ 𝐵)) |
7 | | vex 2715 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
8 | 7 | opres 4874 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → (〈𝑥, 𝑦〉 ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ↔ 〈𝑥, 𝑦〉 ∈ 𝐹)) |
9 | | vex 2715 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
10 | 9 | opres 4874 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → (〈𝑥, 𝑧〉 ∈ (𝐺 ↾ (𝐴 ∩ 𝐵)) ↔ 〈𝑥, 𝑧〉 ∈ 𝐺)) |
11 | 8, 10 | anbi12d 465 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → ((〈𝑥, 𝑦〉 ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ 〈𝑥, 𝑧〉 ∈ (𝐺 ↾ (𝐴 ∩ 𝐵))) ↔ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺))) |
12 | 11 | biimprd 157 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) → (〈𝑥, 𝑦〉 ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ 〈𝑥, 𝑧〉 ∈ (𝐺 ↾ (𝐴 ∩ 𝐵))))) |
13 | 6, 12 | syl 14 |
. . . 4
⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) → (〈𝑥, 𝑦〉 ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ 〈𝑥, 𝑧〉 ∈ (𝐺 ↾ (𝐴 ∩ 𝐵))))) |
14 | 13 | ex 114 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) → (〈𝑥, 𝑦〉 ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ 〈𝑥, 𝑧〉 ∈ (𝐺 ↾ (𝐴 ∩ 𝐵)))))) |
15 | 14 | pm2.43d 50 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) → (〈𝑥, 𝑦〉 ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ 〈𝑥, 𝑧〉 ∈ (𝐺 ↾ (𝐴 ∩ 𝐵))))) |
16 | | resss 4889 |
. . . 4
⊢ (𝐹 ↾ (𝐴 ∩ 𝐵)) ⊆ 𝐹 |
17 | 16 | sseli 3124 |
. . 3
⊢
(〈𝑥, 𝑦〉 ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) → 〈𝑥, 𝑦〉 ∈ 𝐹) |
18 | | resss 4889 |
. . . 4
⊢ (𝐺 ↾ (𝐴 ∩ 𝐵)) ⊆ 𝐺 |
19 | 18 | sseli 3124 |
. . 3
⊢
(〈𝑥, 𝑧〉 ∈ (𝐺 ↾ (𝐴 ∩ 𝐵)) → 〈𝑥, 𝑧〉 ∈ 𝐺) |
20 | 17, 19 | anim12i 336 |
. 2
⊢
((〈𝑥, 𝑦〉 ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ 〈𝑥, 𝑧〉 ∈ (𝐺 ↾ (𝐴 ∩ 𝐵))) → (〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺)) |
21 | 15, 20 | impbid1 141 |
1
⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((〈𝑥, 𝑦〉 ∈ 𝐹 ∧ 〈𝑥, 𝑧〉 ∈ 𝐺) ↔ (〈𝑥, 𝑦〉 ∈ (𝐹 ↾ (𝐴 ∩ 𝐵)) ∧ 〈𝑥, 𝑧〉 ∈ (𝐺 ↾ (𝐴 ∩ 𝐵))))) |