Proof of Theorem bnj1136
| Step | Hyp | Ref
| Expression |
| 1 | | bnj1136.2 |
. . . 4
⊢ (𝜃 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴)) |
| 2 | 1 | biimpri 228 |
. . 3
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝜃) |
| 3 | | bnj1136.1 |
. . . . 5
⊢ 𝐵 = ( pred(𝑋, 𝐴, 𝑅) ∪ ∪
𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) |
| 4 | | bnj1148 35010 |
. . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ∈ V) |
| 5 | | bnj893 34942 |
. . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) ∈ V) |
| 6 | | simp1 1137 |
. . . . . . . . . 10
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅)) → 𝑅 FrSe 𝐴) |
| 7 | | bnj1127 35005 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → 𝑦 ∈ 𝐴) |
| 8 | 7 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅)) → 𝑦 ∈ 𝐴) |
| 9 | | bnj893 34942 |
. . . . . . . . . 10
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴) → trCl(𝑦, 𝐴, 𝑅) ∈ V) |
| 10 | 6, 8, 9 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ∈ V) |
| 11 | 10 | 3expia 1122 |
. . . . . . . 8
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ∈ V)) |
| 12 | 11 | ralrimiv 3145 |
. . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ∈ V) |
| 13 | | iunexg 7988 |
. . . . . . 7
⊢ ((
trCl(𝑋, 𝐴, 𝑅) ∈ V ∧ ∀𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ∈ V) → ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ∈ V) |
| 14 | 5, 12, 13 | syl2anc 584 |
. . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∪
𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ∈ V) |
| 15 | 4, 14 | bnj1149 34806 |
. . . . 5
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ( pred(𝑋, 𝐴, 𝑅) ∪ ∪
𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ∈ V) |
| 16 | 3, 15 | eqeltrid 2845 |
. . . 4
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ∈ V) |
| 17 | 3 | bnj1137 35009 |
. . . 4
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → TrFo(𝐵, 𝐴, 𝑅)) |
| 18 | 3 | bnj931 34784 |
. . . . 5
⊢
pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵 |
| 19 | 18 | a1i 11 |
. . . 4
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵) |
| 20 | | bnj1136.3 |
. . . 4
⊢ (𝜏 ↔ (𝐵 ∈ V ∧ TrFo(𝐵, 𝐴, 𝑅) ∧ pred(𝑋, 𝐴, 𝑅) ⊆ 𝐵)) |
| 21 | 16, 17, 19, 20 | syl3anbrc 1344 |
. . 3
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝜏) |
| 22 | 1, 20 | bnj1124 35002 |
. . 3
⊢ ((𝜃 ∧ 𝜏) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵) |
| 23 | 2, 21, 22 | syl2anc 584 |
. 2
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐵) |
| 24 | | bnj906 34944 |
. . . 4
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → pred(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅)) |
| 25 | | bnj1125 35006 |
. . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl(𝑋, 𝐴, 𝑅)) → trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅)) |
| 26 | 25 | 3expia 1122 |
. . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑦 ∈ trCl(𝑋, 𝐴, 𝑅) → trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅))) |
| 27 | 26 | ralrimiv 3145 |
. . . . 5
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅)) |
| 28 | | ss2iun 5010 |
. . . . . 6
⊢
(∀𝑦 ∈
trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅) → ∪
𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑋, 𝐴, 𝑅)) |
| 29 | | bnj1143 34804 |
. . . . . 6
⊢ ∪ 𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑋, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅) |
| 30 | 28, 29 | sstrdi 3996 |
. . . . 5
⊢
(∀𝑦 ∈
trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅) → ∪
𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅)) |
| 31 | 27, 30 | syl 17 |
. . . 4
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∪
𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅) ⊆ trCl(𝑋, 𝐴, 𝑅)) |
| 32 | 24, 31 | unssd 4192 |
. . 3
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ( pred(𝑋, 𝐴, 𝑅) ∪ ∪
𝑦 ∈ trCl (𝑋, 𝐴, 𝑅) trCl(𝑦, 𝐴, 𝑅)) ⊆ trCl(𝑋, 𝐴, 𝑅)) |
| 33 | 3, 32 | eqsstrid 4022 |
. 2
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐵 ⊆ trCl(𝑋, 𝐴, 𝑅)) |
| 34 | 23, 33 | eqssd 4001 |
1
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → trCl(𝑋, 𝐴, 𝑅) = 𝐵) |