| Step | Hyp | Ref
| Expression |
| 1 | | eldifsn 4786 |
. . . 4
⊢ (𝑥 ∈ (𝐴 ∖ {∩ 𝐴}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ≠ ∩ 𝐴)) |
| 2 | | onnmin 7818 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ ∩ 𝐴) |
| 3 | 2 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥 ∈ ∩ 𝐴) |
| 4 | | oninton 7815 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ On) |
| 5 | | ssel2 3978 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On) |
| 6 | 5 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ On) |
| 7 | | ontri1 6418 |
. . . . . . . . . . 11
⊢ ((∩ 𝐴
∈ On ∧ 𝑥 ∈
On) → (∩ 𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ ∩ 𝐴)) |
| 8 | | onsseleq 6425 |
. . . . . . . . . . 11
⊢ ((∩ 𝐴
∈ On ∧ 𝑥 ∈
On) → (∩ 𝐴 ⊆ 𝑥 ↔ (∩ 𝐴 ∈ 𝑥 ∨ ∩ 𝐴 = 𝑥))) |
| 9 | 7, 8 | bitr3d 281 |
. . . . . . . . . 10
⊢ ((∩ 𝐴
∈ On ∧ 𝑥 ∈
On) → (¬ 𝑥 ∈
∩ 𝐴 ↔ (∩ 𝐴 ∈ 𝑥 ∨ ∩ 𝐴 = 𝑥))) |
| 10 | 4, 6, 9 | syl2an2r 685 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (¬ 𝑥 ∈ ∩ 𝐴 ↔ (∩ 𝐴
∈ 𝑥 ∨ ∩ 𝐴 =
𝑥))) |
| 11 | 3, 10 | mpbid 232 |
. . . . . . . 8
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (∩ 𝐴 ∈ 𝑥 ∨ ∩ 𝐴 = 𝑥)) |
| 12 | 11 | ord 865 |
. . . . . . 7
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (¬ ∩
𝐴 ∈ 𝑥 → ∩ 𝐴 = 𝑥)) |
| 13 | | eqcom 2744 |
. . . . . . 7
⊢ (∩ 𝐴 =
𝑥 ↔ 𝑥 = ∩ 𝐴) |
| 14 | 12, 13 | imbitrdi 251 |
. . . . . 6
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (¬ ∩
𝐴 ∈ 𝑥 → 𝑥 = ∩ 𝐴)) |
| 15 | 14 | necon1ad 2957 |
. . . . 5
⊢ (((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (𝑥 ≠ ∩ 𝐴 → ∩ 𝐴
∈ 𝑥)) |
| 16 | 15 | expimpd 453 |
. . . 4
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ ∩ 𝐴) → ∩ 𝐴
∈ 𝑥)) |
| 17 | 1, 16 | biimtrid 242 |
. . 3
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → (𝑥 ∈ (𝐴 ∖ {∩ 𝐴}) → ∩ 𝐴
∈ 𝑥)) |
| 18 | 17 | ralrimiv 3145 |
. 2
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) →
∀𝑥 ∈ (𝐴 ∖ {∩ 𝐴})∩ 𝐴 ∈ 𝑥) |
| 19 | | intex 5344 |
. . . 4
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴
∈ V) |
| 20 | | elintg 4954 |
. . . 4
⊢ (∩ 𝐴
∈ V → (∩ 𝐴 ∈ ∩ (𝐴 ∖ {∩ 𝐴})
↔ ∀𝑥 ∈
(𝐴 ∖ {∩ 𝐴})∩ 𝐴 ∈ 𝑥)) |
| 21 | 19, 20 | sylbi 217 |
. . 3
⊢ (𝐴 ≠ ∅ → (∩ 𝐴
∈ ∩ (𝐴 ∖ {∩ 𝐴}) ↔ ∀𝑥 ∈ (𝐴 ∖ {∩ 𝐴})∩
𝐴 ∈ 𝑥)) |
| 22 | 21 | adantl 481 |
. 2
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → (∩ 𝐴
∈ ∩ (𝐴 ∖ {∩ 𝐴}) ↔ ∀𝑥 ∈ (𝐴 ∖ {∩ 𝐴})∩
𝐴 ∈ 𝑥)) |
| 23 | 18, 22 | mpbird 257 |
1
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ ∩ (𝐴 ∖ {∩ 𝐴})) |