Step | Hyp | Ref
| Expression |
1 | | tglng.p |
. . . . . . . 8
⊢ 𝑃 = (Base‘𝐺) |
2 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘𝐺)
∈ V |
3 | 1, 2 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑃 ∈ V |
4 | 3 | rabex 4740 |
. . . . . 6
⊢ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))} ∈ V |
5 | 4 | rgen2w 2909 |
. . . . 5
⊢
∀𝑥 ∈
𝑃 ∀𝑦 ∈ (𝑃 ∖ {𝑥}){𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))} ∈ V |
6 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) |
7 | 6 | fmpt2x 7125 |
. . . . 5
⊢
(∀𝑥 ∈
𝑃 ∀𝑦 ∈ (𝑃 ∖ {𝑥}){𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))} ∈ V ↔ (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}):∪
𝑥 ∈ 𝑃 ({𝑥} × (𝑃 ∖ {𝑥}))⟶V) |
8 | 5, 7 | mpbi 219 |
. . . 4
⊢ (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}):∪
𝑥 ∈ 𝑃 ({𝑥} × (𝑃 ∖ {𝑥}))⟶V |
9 | | ffn 5958 |
. . . 4
⊢ ((𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}):∪
𝑥 ∈ 𝑃 ({𝑥} × (𝑃 ∖ {𝑥}))⟶V → (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) Fn ∪
𝑥 ∈ 𝑃 ({𝑥} × (𝑃 ∖ {𝑥}))) |
10 | 8, 9 | ax-mp 5 |
. . 3
⊢ (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) Fn ∪
𝑥 ∈ 𝑃 ({𝑥} × (𝑃 ∖ {𝑥})) |
11 | | xpdifid 5481 |
. . . 4
⊢ ∪ 𝑥 ∈ 𝑃 ({𝑥} × (𝑃 ∖ {𝑥})) = ((𝑃 × 𝑃) ∖ I ) |
12 | 11 | fneq2i 5900 |
. . 3
⊢ ((𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) Fn ∪
𝑥 ∈ 𝑃 ({𝑥} × (𝑃 ∖ {𝑥})) ↔ (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) Fn ((𝑃 × 𝑃) ∖ I )) |
13 | 10, 12 | mpbi 219 |
. 2
⊢ (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) Fn ((𝑃 × 𝑃) ∖ I ) |
14 | | tglng.l |
. . . 4
⊢ 𝐿 = (LineG‘𝐺) |
15 | | tglng.i |
. . . 4
⊢ 𝐼 = (Itv‘𝐺) |
16 | 1, 14, 15 | tglng 25241 |
. . 3
⊢ (𝐺 ∈ TarskiG → 𝐿 = (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))})) |
17 | 16 | fneq1d 5895 |
. 2
⊢ (𝐺 ∈ TarskiG → (𝐿 Fn ((𝑃 × 𝑃) ∖ I ) ↔ (𝑥 ∈ 𝑃, 𝑦 ∈ (𝑃 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑃 ∣ (𝑧 ∈ (𝑥𝐼𝑦) ∨ 𝑥 ∈ (𝑧𝐼𝑦) ∨ 𝑦 ∈ (𝑥𝐼𝑧))}) Fn ((𝑃 × 𝑃) ∖ I ))) |
18 | 13, 17 | mpbiri 247 |
1
⊢ (𝐺 ∈ TarskiG → 𝐿 Fn ((𝑃 × 𝑃) ∖ I )) |