Proof of Theorem bnj1173
| Step | Hyp | Ref
| Expression |
| 1 | | bnj1173.5 |
. . 3
⊢ (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) ∧ (𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴)) |
| 2 | | 3simpc 1151 |
. . . 4
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) ∧ (𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴)) |
| 3 | | bnj1173.9 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝑅 FrSe 𝐴) |
| 4 | 3 | 3adant3 1133 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → 𝑅 FrSe 𝐴) |
| 5 | | bnj1173.17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐴) |
| 6 | 5 | 3adant3 1133 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → 𝑋 ∈ 𝐴) |
| 7 | | elin 3967 |
. . . . . . . . 9
⊢ (𝑧 ∈ ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵) ↔ (𝑧 ∈ trCl(𝑋, 𝐴, 𝑅) ∧ 𝑧 ∈ 𝐵)) |
| 8 | 7 | simplbi 497 |
. . . . . . . 8
⊢ (𝑧 ∈ ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵) → 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) |
| 9 | | bnj1173.3 |
. . . . . . . 8
⊢ 𝐶 = ( trCl(𝑋, 𝐴, 𝑅) ∩ 𝐵) |
| 10 | 8, 9 | eleq2s 2859 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐶 → 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) |
| 11 | 10 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) |
| 12 | | pm3.21 471 |
. . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) → (((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → (((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ∧ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅))))) |
| 13 | 4, 6, 11, 12 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → (((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → (((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ∧ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅))))) |
| 14 | | bnj170 34712 |
. . . . 5
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) ∧ (𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ↔ (((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ∧ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)))) |
| 15 | 13, 14 | imbitrrdi 252 |
. . . 4
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → (((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) → ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) ∧ (𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴))) |
| 16 | 2, 15 | impbid2 226 |
. . 3
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑧 ∈ trCl(𝑋, 𝐴, 𝑅)) ∧ (𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴))) |
| 17 | 1, 16 | bitrid 283 |
. 2
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → (𝜃 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴))) |
| 18 | | bnj1147 35008 |
. . . . 5
⊢
trCl(𝑋, 𝐴, 𝑅) ⊆ 𝐴 |
| 19 | 18, 11 | bnj1213 34812 |
. . . 4
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ 𝐴) |
| 20 | 4, 19 | jca 511 |
. . 3
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → (𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴)) |
| 21 | 20 | biantrurd 532 |
. 2
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → (𝑤 ∈ 𝐴 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐴))) |
| 22 | 17, 21 | bitr4d 282 |
1
⊢ ((𝜑 ∧ 𝜓 ∧ 𝑧 ∈ 𝐶) → (𝜃 ↔ 𝑤 ∈ 𝐴)) |