Proof of Theorem tc2
| Step | Hyp | Ref
| Expression |
| 1 | | tc2.1 |
. . . . 5
⊢ 𝐴 ∈ V |
| 2 | | tcvalg 9778 |
. . . . 5
⊢ (𝐴 ∈ V → (TC‘𝐴) = ∩
{𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)}) |
| 3 | 1, 2 | ax-mp 5 |
. . . 4
⊢
(TC‘𝐴) = ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} |
| 4 | | trss 5270 |
. . . . . . 7
⊢ (Tr 𝑥 → (𝐴 ∈ 𝑥 → 𝐴 ⊆ 𝑥)) |
| 5 | 4 | imdistanri 569 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑥 ∧ Tr 𝑥) → (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)) |
| 6 | 5 | ss2abi 4067 |
. . . . 5
⊢ {𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} ⊆ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} |
| 7 | | intss 4969 |
. . . . 5
⊢ ({𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} ⊆ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} → ∩ {𝑥 ∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∩
{𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)}) |
| 8 | 6, 7 | ax-mp 5 |
. . . 4
⊢ ∩ {𝑥
∣ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∩
{𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} |
| 9 | 3, 8 | eqsstri 4030 |
. . 3
⊢
(TC‘𝐴) ⊆
∩ {𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} |
| 10 | 1 | elintab 4958 |
. . . . 5
⊢ (𝐴 ∈ ∩ {𝑥
∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} ↔ ∀𝑥((𝐴 ∈ 𝑥 ∧ Tr 𝑥) → 𝐴 ∈ 𝑥)) |
| 11 | | simpl 482 |
. . . . 5
⊢ ((𝐴 ∈ 𝑥 ∧ Tr 𝑥) → 𝐴 ∈ 𝑥) |
| 12 | 10, 11 | mpgbir 1799 |
. . . 4
⊢ 𝐴 ∈ ∩ {𝑥
∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} |
| 13 | 1 | snss 4785 |
. . . 4
⊢ (𝐴 ∈ ∩ {𝑥
∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} ↔ {𝐴} ⊆ ∩
{𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)}) |
| 14 | 12, 13 | mpbi 230 |
. . 3
⊢ {𝐴} ⊆ ∩ {𝑥
∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} |
| 15 | 9, 14 | unssi 4191 |
. 2
⊢
((TC‘𝐴) ∪
{𝐴}) ⊆ ∩ {𝑥
∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} |
| 16 | 1 | snid 4662 |
. . . . 5
⊢ 𝐴 ∈ {𝐴} |
| 17 | | elun2 4183 |
. . . . 5
⊢ (𝐴 ∈ {𝐴} → 𝐴 ∈ ((TC‘𝐴) ∪ {𝐴})) |
| 18 | 16, 17 | ax-mp 5 |
. . . 4
⊢ 𝐴 ∈ ((TC‘𝐴) ∪ {𝐴}) |
| 19 | | uniun 4930 |
. . . . . . 7
⊢ ∪ ((TC‘𝐴) ∪ {𝐴}) = (∪
(TC‘𝐴) ∪ ∪ {𝐴}) |
| 20 | | tctr 9780 |
. . . . . . . . 9
⊢ Tr
(TC‘𝐴) |
| 21 | | df-tr 5260 |
. . . . . . . . 9
⊢ (Tr
(TC‘𝐴) ↔ ∪ (TC‘𝐴) ⊆ (TC‘𝐴)) |
| 22 | 20, 21 | mpbi 230 |
. . . . . . . 8
⊢ ∪ (TC‘𝐴) ⊆ (TC‘𝐴) |
| 23 | 1 | unisn 4926 |
. . . . . . . . 9
⊢ ∪ {𝐴}
= 𝐴 |
| 24 | | tcid 9779 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → 𝐴 ⊆ (TC‘𝐴)) |
| 25 | 1, 24 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝐴 ⊆ (TC‘𝐴) |
| 26 | 23, 25 | eqsstri 4030 |
. . . . . . . 8
⊢ ∪ {𝐴}
⊆ (TC‘𝐴) |
| 27 | 22, 26 | unssi 4191 |
. . . . . . 7
⊢ (∪ (TC‘𝐴) ∪ ∪ {𝐴}) ⊆ (TC‘𝐴) |
| 28 | 19, 27 | eqsstri 4030 |
. . . . . 6
⊢ ∪ ((TC‘𝐴) ∪ {𝐴}) ⊆ (TC‘𝐴) |
| 29 | | ssun1 4178 |
. . . . . 6
⊢
(TC‘𝐴) ⊆
((TC‘𝐴) ∪ {𝐴}) |
| 30 | 28, 29 | sstri 3993 |
. . . . 5
⊢ ∪ ((TC‘𝐴) ∪ {𝐴}) ⊆ ((TC‘𝐴) ∪ {𝐴}) |
| 31 | | df-tr 5260 |
. . . . 5
⊢ (Tr
((TC‘𝐴) ∪ {𝐴}) ↔ ∪ ((TC‘𝐴) ∪ {𝐴}) ⊆ ((TC‘𝐴) ∪ {𝐴})) |
| 32 | 30, 31 | mpbir 231 |
. . . 4
⊢ Tr
((TC‘𝐴) ∪ {𝐴}) |
| 33 | | fvex 6919 |
. . . . . 6
⊢
(TC‘𝐴) ∈
V |
| 34 | | snex 5436 |
. . . . . 6
⊢ {𝐴} ∈ V |
| 35 | 33, 34 | unex 7764 |
. . . . 5
⊢
((TC‘𝐴) ∪
{𝐴}) ∈
V |
| 36 | | eleq2 2830 |
. . . . . 6
⊢ (𝑥 = ((TC‘𝐴) ∪ {𝐴}) → (𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ((TC‘𝐴) ∪ {𝐴}))) |
| 37 | | treq 5267 |
. . . . . 6
⊢ (𝑥 = ((TC‘𝐴) ∪ {𝐴}) → (Tr 𝑥 ↔ Tr ((TC‘𝐴) ∪ {𝐴}))) |
| 38 | 36, 37 | anbi12d 632 |
. . . . 5
⊢ (𝑥 = ((TC‘𝐴) ∪ {𝐴}) → ((𝐴 ∈ 𝑥 ∧ Tr 𝑥) ↔ (𝐴 ∈ ((TC‘𝐴) ∪ {𝐴}) ∧ Tr ((TC‘𝐴) ∪ {𝐴})))) |
| 39 | 35, 38 | elab 3679 |
. . . 4
⊢
(((TC‘𝐴) ∪
{𝐴}) ∈ {𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} ↔ (𝐴 ∈ ((TC‘𝐴) ∪ {𝐴}) ∧ Tr ((TC‘𝐴) ∪ {𝐴}))) |
| 40 | 18, 32, 39 | mpbir2an 711 |
. . 3
⊢
((TC‘𝐴) ∪
{𝐴}) ∈ {𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} |
| 41 | | intss1 4963 |
. . 3
⊢
(((TC‘𝐴) ∪
{𝐴}) ∈ {𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} → ∩ {𝑥 ∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} ⊆ ((TC‘𝐴) ∪ {𝐴})) |
| 42 | 40, 41 | ax-mp 5 |
. 2
⊢ ∩ {𝑥
∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} ⊆ ((TC‘𝐴) ∪ {𝐴}) |
| 43 | 15, 42 | eqssi 4000 |
1
⊢
((TC‘𝐴) ∪
{𝐴}) = ∩ {𝑥
∣ (𝐴 ∈ 𝑥 ∧ Tr 𝑥)} |