Step | Hyp | Ref
| Expression |
1 | | eldifsn 4260 |
. . . 4
⊢ (𝑥 ∈ (𝐴 ∖ {∩ 𝐴}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ≠ ∩ 𝐴)) |
2 | | onnmin 6895 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ ∩ 𝐴) |
3 | 2 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ ∩ 𝐴) |
4 | | oninton 6892 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ On) |
5 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → ∩ 𝐴 ∈ On) |
6 | | ssel2 3563 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On) |
7 | 6 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On) |
8 | | ontri1 5674 |
. . . . . . . . . . 11
⊢ ((∩ 𝐴
∈ On ∧ 𝑥 ∈
On) → (∩ 𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ ∩ 𝐴)) |
9 | | onsseleq 5682 |
. . . . . . . . . . 11
⊢ ((∩ 𝐴
∈ On ∧ 𝑥 ∈
On) → (∩ 𝐴 ⊆ 𝑥 ↔ (∩ 𝐴 ∈ 𝑥 ∨ ∩ 𝐴 = 𝑥))) |
10 | 8, 9 | bitr3d 269 |
. . . . . . . . . 10
⊢ ((∩ 𝐴
∈ On ∧ 𝑥 ∈
On) → (¬ 𝑥 ∈
∩ 𝐴 ↔ (∩ 𝐴 ∈ 𝑥 ∨ ∩ 𝐴 = 𝑥))) |
11 | 5, 7, 10 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (¬ 𝑥 ∈ ∩ 𝐴 ↔ (∩ 𝐴
∈ 𝑥 ∨ ∩ 𝐴 =
𝑥))) |
12 | 3, 11 | mpbid 221 |
. . . . . . . 8
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (∩ 𝐴 ∈ 𝑥 ∨ ∩ 𝐴 = 𝑥)) |
13 | 12 | ord 391 |
. . . . . . 7
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (¬ ∩
𝐴 ∈ 𝑥 → ∩ 𝐴 = 𝑥)) |
14 | | eqcom 2617 |
. . . . . . 7
⊢ (∩ 𝐴 =
𝑥 ↔ 𝑥 = ∩ 𝐴) |
15 | 13, 14 | syl6ib 240 |
. . . . . 6
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (¬ ∩
𝐴 ∈ 𝑥 → 𝑥 = ∩ 𝐴)) |
16 | 15 | necon1ad 2799 |
. . . . 5
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≠ ∩ 𝐴 → ∩ 𝐴
∈ 𝑥)) |
17 | 16 | expimpd 627 |
. . . 4
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ ∩ 𝐴) → ∩ 𝐴
∈ 𝑥)) |
18 | 1, 17 | syl5bi 231 |
. . 3
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → (𝑥 ∈ (𝐴 ∖ {∩ 𝐴}) → ∩ 𝐴
∈ 𝑥)) |
19 | 18 | ralrimiv 2948 |
. 2
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) →
∀𝑥 ∈ (𝐴 ∖ {∩ 𝐴})∩ 𝐴 ∈ 𝑥) |
20 | | intex 4747 |
. . . 4
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴
∈ V) |
21 | | elintg 4418 |
. . . 4
⊢ (∩ 𝐴
∈ V → (∩ 𝐴 ∈ ∩ (𝐴 ∖ {∩ 𝐴})
↔ ∀𝑥 ∈
(𝐴 ∖ {∩ 𝐴})∩ 𝐴 ∈ 𝑥)) |
22 | 20, 21 | sylbi 206 |
. . 3
⊢ (𝐴 ≠ ∅ → (∩ 𝐴
∈ ∩ (𝐴 ∖ {∩ 𝐴}) ↔ ∀𝑥 ∈ (𝐴 ∖ {∩ 𝐴})∩
𝐴 ∈ 𝑥)) |
23 | 22 | adantl 481 |
. 2
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → (∩ 𝐴
∈ ∩ (𝐴 ∖ {∩ 𝐴}) ↔ ∀𝑥 ∈ (𝐴 ∖ {∩ 𝐴})∩
𝐴 ∈ 𝑥)) |
24 | 19, 23 | mpbird 246 |
1
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ ∩ (𝐴 ∖ {∩ 𝐴})) |