| Step | Hyp | Ref
| Expression |
| 1 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 2 | | dfon2lem3 35786 |
. . . . . . 7
⊢ (𝑥 ∈ V → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧))) |
| 3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (Tr 𝑥 ∧ ∀𝑧 ∈ 𝑥 ¬ 𝑧 ∈ 𝑧)) |
| 4 | 3 | simpld 494 |
. . . . 5
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr 𝑥) |
| 5 | 4 | ralimi 3083 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐴 Tr 𝑥) |
| 6 | | trint 5277 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 Tr 𝑥 → Tr ∩ 𝐴) |
| 7 | 5, 6 | syl 17 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → Tr ∩
𝐴) |
| 8 | 7 | adantl 481 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → Tr ∩
𝐴) |
| 9 | 1 | dfon2lem7 35790 |
. . . . . . 7
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 10 | 9 | alrimiv 1927 |
. . . . . 6
⊢
(∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 11 | 10 | ralimi 3083 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 12 | | df-ral 3062 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))) |
| 13 | | 19.21v 1939 |
. . . . . . . 8
⊢
(∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) ↔ (𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))) |
| 14 | 13 | albii 1819 |
. . . . . . 7
⊢
(∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))) |
| 15 | 12, 14 | bitr4i 278 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))) |
| 16 | | impexp 450 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))) |
| 17 | 16 | 2albii 1820 |
. . . . . . 7
⊢
(∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)))) |
| 18 | | eluni2 4911 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ∪ 𝐴
↔ ∃𝑥 ∈
𝐴 𝑤 ∈ 𝑥) |
| 19 | 18 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ∪ 𝐴
→ ∃𝑥 ∈
𝐴 𝑤 ∈ 𝑥) |
| 20 | 19 | imim1i 63 |
. . . . . . . . 9
⊢
((∃𝑥 ∈
𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → (𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 21 | 20 | alimi 1811 |
. . . . . . . 8
⊢
(∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤(𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 22 | | alcom 2159 |
. . . . . . . . 9
⊢
(∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 23 | | 19.23v 1942 |
. . . . . . . . . . 11
⊢
(∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 24 | | df-rex 3071 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
𝐴 𝑤 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥)) |
| 25 | 24 | imbi1i 349 |
. . . . . . . . . . 11
⊢
((∃𝑥 ∈
𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 26 | 23, 25 | bitr4i 278 |
. . . . . . . . . 10
⊢
(∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ (∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 27 | 26 | albii 1819 |
. . . . . . . . 9
⊢
(∀𝑤∀𝑥((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 28 | 22, 27 | bitri 275 |
. . . . . . . 8
⊢
(∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) ↔ ∀𝑤(∃𝑥 ∈ 𝐴 𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 29 | | df-ral 3062 |
. . . . . . . 8
⊢
(∀𝑤 ∈
∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) ↔ ∀𝑤(𝑤 ∈ ∪ 𝐴 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 30 | 21, 28, 29 | 3imtr4i 292 |
. . . . . . 7
⊢
(∀𝑥∀𝑤((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) |
| 31 | 17, 30 | sylbir 235 |
. . . . . 6
⊢
(∀𝑥∀𝑤(𝑥 ∈ 𝐴 → (𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) |
| 32 | 15, 31 | sylbi 217 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) |
| 33 | 11, 32 | syl 17 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) |
| 34 | 33 | adantl 481 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) |
| 35 | | intssuni 4970 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ∩ 𝐴
⊆ ∪ 𝐴) |
| 36 | | ssralv 4052 |
. . . . 5
⊢ (∩ 𝐴
⊆ ∪ 𝐴 → (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 37 | 35, 36 | syl 17 |
. . . 4
⊢ (𝐴 ≠ ∅ →
(∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 38 | 37 | adantr 480 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑤 ∈ ∪ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤))) |
| 39 | 34, 38 | mpd 15 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) |
| 40 | | dfon2lem6 35789 |
. . 3
⊢ ((Tr
∩ 𝐴 ∧ ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) |
| 41 | | intex 5344 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ ∅ ↔ ∩ 𝐴
∈ V) |
| 42 | | dfon2lem3 35786 |
. . . . . . . . . . 11
⊢ (∩ 𝐴
∈ V → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → (Tr ∩ 𝐴
∧ ∀𝑡 ∈
∩ 𝐴 ¬ 𝑡 ∈ 𝑡))) |
| 43 | 41, 42 | sylbi 217 |
. . . . . . . . . 10
⊢ (𝐴 ≠ ∅ →
(∀𝑧((𝑧 ⊊ ∩ 𝐴
∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)
→ (Tr ∩ 𝐴 ∧ ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡))) |
| 44 | 43 | imp 406 |
. . . . . . . . 9
⊢ ((𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊊ ∩ 𝐴
∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴))
→ (Tr ∩ 𝐴 ∧ ∀𝑡 ∈ ∩ 𝐴 ¬ 𝑡 ∈ 𝑡)) |
| 45 | 44 | simprd 495 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊊ ∩ 𝐴
∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴))
→ ∀𝑡 ∈
∩ 𝐴 ¬ 𝑡 ∈ 𝑡) |
| 46 | | untelirr 35708 |
. . . . . . . 8
⊢
(∀𝑡 ∈
∩ 𝐴 ¬ 𝑡 ∈ 𝑡 → ¬ ∩
𝐴 ∈ ∩ 𝐴) |
| 47 | 45, 46 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊊ ∩ 𝐴
∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴))
→ ¬ ∩ 𝐴 ∈ ∩ 𝐴) |
| 48 | 47 | adantlr 715 |
. . . . . 6
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ¬ ∩ 𝐴
∈ ∩ 𝐴) |
| 49 | | risset 3233 |
. . . . . . . . . 10
⊢ (∩ 𝐴
∈ 𝐴 ↔
∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴) |
| 50 | 49 | notbii 320 |
. . . . . . . . 9
⊢ (¬
∩ 𝐴 ∈ 𝐴 ↔ ¬ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴) |
| 51 | | ralnex 3072 |
. . . . . . . . 9
⊢
(∀𝑡 ∈
𝐴 ¬ 𝑡 = ∩ 𝐴 ↔ ¬ ∃𝑡 ∈ 𝐴 𝑡 = ∩ 𝐴) |
| 52 | 50, 51 | bitr4i 278 |
. . . . . . . 8
⊢ (¬
∩ 𝐴 ∈ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴) |
| 53 | | eqcom 2744 |
. . . . . . . . . . . 12
⊢ (𝑡 = ∩
𝐴 ↔ ∩ 𝐴 =
𝑡) |
| 54 | 53 | notbii 320 |
. . . . . . . . . . 11
⊢ (¬
𝑡 = ∩ 𝐴
↔ ¬ ∩ 𝐴 = 𝑡) |
| 55 | 44 | simpld 494 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊊ ∩ 𝐴
∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴))
→ Tr ∩ 𝐴) |
| 56 | 55 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → Tr ∩ 𝐴) |
| 57 | | psseq2 4091 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑡 → (𝑦 ⊊ 𝑥 ↔ 𝑦 ⊊ 𝑡)) |
| 58 | 57 | anbi1d 631 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → ((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) ↔ (𝑦 ⊊ 𝑡 ∧ Tr 𝑦))) |
| 59 | | elequ2 2123 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑡 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑡)) |
| 60 | 58, 59 | imbi12d 344 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑡 → (((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ ((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡))) |
| 61 | 60 | albidv 1920 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑡 → (∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) ↔ ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡))) |
| 62 | 61 | rspccv 3619 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → (𝑡 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡))) |
| 63 | 62 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡))) |
| 64 | | intss1 4963 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑡) |
| 65 | | dfpss2 4088 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∩ 𝐴
⊊ 𝑡 ↔ (∩ 𝐴
⊆ 𝑡 ∧ ¬ ∩ 𝐴 =
𝑡)) |
| 66 | | psseq1 4090 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = ∩
𝐴 → (𝑦 ⊊ 𝑡 ↔ ∩ 𝐴 ⊊ 𝑡)) |
| 67 | | treq 5267 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = ∩
𝐴 → (Tr 𝑦 ↔ Tr ∩ 𝐴)) |
| 68 | 66, 67 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = ∩
𝐴 → ((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) ↔ (∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴))) |
| 69 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = ∩
𝐴 → (𝑦 ∈ 𝑡 ↔ ∩ 𝐴 ∈ 𝑡)) |
| 70 | 68, 69 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = ∩
𝐴 → (((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) ↔ ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴
∈ 𝑡))) |
| 71 | 70 | spcgv 3596 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∩ 𝐴
∈ V → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴
∈ 𝑡))) |
| 72 | 41, 71 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ≠ ∅ →
(∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → ((∩ 𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴) → ∩ 𝐴
∈ 𝑡))) |
| 73 | 72 | imp 406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)) → ((∩
𝐴 ⊊ 𝑡 ∧ Tr ∩ 𝐴)
→ ∩ 𝐴 ∈ 𝑡)) |
| 74 | 73 | expd 415 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)) → (∩ 𝐴 ⊊ 𝑡 → (Tr ∩
𝐴 → ∩ 𝐴
∈ 𝑡))) |
| 75 | 65, 74 | biimtrrid 243 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡)) → ((∩
𝐴 ⊆ 𝑡 ∧ ¬ ∩ 𝐴 =
𝑡) → (Tr ∩ 𝐴
→ ∩ 𝐴 ∈ 𝑡))) |
| 76 | 75 | exp4b 430 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ≠ ∅ →
(∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (∩ 𝐴 ⊆ 𝑡 → (¬ ∩
𝐴 = 𝑡 → (Tr ∩
𝐴 → ∩ 𝐴
∈ 𝑡))))) |
| 77 | 76 | com45 97 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ≠ ∅ →
(∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (∩ 𝐴 ⊆ 𝑡 → (Tr ∩
𝐴 → (¬ ∩ 𝐴 =
𝑡 → ∩ 𝐴
∈ 𝑡))))) |
| 78 | 77 | com23 86 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ≠ ∅ → (∩ 𝐴
⊆ 𝑡 →
(∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (Tr ∩
𝐴 → (¬ ∩ 𝐴 =
𝑡 → ∩ 𝐴
∈ 𝑡))))) |
| 79 | 64, 78 | syl5 34 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ≠ ∅ → (𝑡 ∈ 𝐴 → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (Tr ∩
𝐴 → (¬ ∩ 𝐴 =
𝑡 → ∩ 𝐴
∈ 𝑡))))) |
| 80 | 79 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → (∀𝑦((𝑦 ⊊ 𝑡 ∧ Tr 𝑦) → 𝑦 ∈ 𝑡) → (Tr ∩
𝐴 → (¬ ∩ 𝐴 =
𝑡 → ∩ 𝐴
∈ 𝑡))))) |
| 81 | 63, 80 | mpdd 43 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (𝑡 ∈ 𝐴 → (Tr ∩
𝐴 → (¬ ∩ 𝐴 =
𝑡 → ∩ 𝐴
∈ 𝑡)))) |
| 82 | 81 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (𝑡 ∈ 𝐴 → (Tr ∩
𝐴 → (¬ ∩ 𝐴 =
𝑡 → ∩ 𝐴
∈ 𝑡)))) |
| 83 | 56, 82 | mpid 44 |
. . . . . . . . . . 11
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (𝑡 ∈ 𝐴 → (¬ ∩
𝐴 = 𝑡 → ∩ 𝐴 ∈ 𝑡))) |
| 84 | 54, 83 | syl7bi 255 |
. . . . . . . . . 10
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (𝑡 ∈ 𝐴 → (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴
∈ 𝑡))) |
| 85 | 84 | ralrimiv 3145 |
. . . . . . . . 9
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ∀𝑡 ∈ 𝐴 (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴
∈ 𝑡)) |
| 86 | | ralim 3086 |
. . . . . . . . 9
⊢
(∀𝑡 ∈
𝐴 (¬ 𝑡 = ∩ 𝐴 → ∩ 𝐴
∈ 𝑡) →
(∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡)) |
| 87 | 85, 86 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (∀𝑡 ∈ 𝐴 ¬ 𝑡 = ∩ 𝐴 → ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡)) |
| 88 | 52, 87 | biimtrid 242 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (¬ ∩ 𝐴
∈ 𝐴 →
∀𝑡 ∈ 𝐴 ∩
𝐴 ∈ 𝑡)) |
| 89 | | elintg 4954 |
. . . . . . . . 9
⊢ (∩ 𝐴
∈ V → (∩ 𝐴 ∈ ∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡)) |
| 90 | 41, 89 | sylbi 217 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ → (∩ 𝐴
∈ ∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡)) |
| 91 | 90 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (∩ 𝐴
∈ ∩ 𝐴 ↔ ∀𝑡 ∈ 𝐴 ∩ 𝐴 ∈ 𝑡)) |
| 92 | 88, 91 | sylibrd 259 |
. . . . . 6
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → (¬ ∩ 𝐴
∈ 𝐴 → ∩ 𝐴
∈ ∩ 𝐴)) |
| 93 | 48, 92 | mt3d 148 |
. . . . 5
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) ∧ ∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴)) → ∩ 𝐴
∈ 𝐴) |
| 94 | 93 | ex 412 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → ∩ 𝐴
∈ 𝐴)) |
| 95 | 94 | ancld 550 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴
∈ 𝐴))) |
| 96 | 40, 95 | syl5 34 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → ((Tr ∩
𝐴 ∧ ∀𝑤 ∈ ∩ 𝐴∀𝑡((𝑡 ⊊ 𝑤 ∧ Tr 𝑡) → 𝑡 ∈ 𝑤)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴
∈ 𝐴))) |
| 97 | 8, 39, 96 | mp2and 699 |
1
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴
∈ 𝐴)) |