Step |
Hyp |
Ref |
Expression |
1 |
|
axtrkg.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
axtrkg.d |
⊢ − = ( dist ‘ 𝐺 ) |
3 |
|
axtrkg.i |
⊢ 𝐼 = ( Itv ‘ 𝐺 ) |
4 |
|
axtrkg.g |
⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) |
5 |
|
axtgpasch.1 |
⊢ ( 𝜑 → 𝑋 ∈ 𝑃 ) |
6 |
|
axtgpasch.2 |
⊢ ( 𝜑 → 𝑌 ∈ 𝑃 ) |
7 |
|
axtgpasch.3 |
⊢ ( 𝜑 → 𝑍 ∈ 𝑃 ) |
8 |
|
axtgpasch.4 |
⊢ ( 𝜑 → 𝑈 ∈ 𝑃 ) |
9 |
|
axtgpasch.5 |
⊢ ( 𝜑 → 𝑉 ∈ 𝑃 ) |
10 |
|
axtgpasch.6 |
⊢ ( 𝜑 → 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ) |
11 |
|
axtgpasch.7 |
⊢ ( 𝜑 → 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) |
12 |
|
df-trkg |
⊢ TarskiG = ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) |
13 |
|
inss1 |
⊢ ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) ⊆ ( TarskiGC ∩ TarskiGB ) |
14 |
|
inss2 |
⊢ ( TarskiGC ∩ TarskiGB ) ⊆ TarskiGB |
15 |
13 14
|
sstri |
⊢ ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) ⊆ TarskiGB |
16 |
12 15
|
eqsstri |
⊢ TarskiG ⊆ TarskiGB |
17 |
16 4
|
sselid |
⊢ ( 𝜑 → 𝐺 ∈ TarskiGB ) |
18 |
1 2 3
|
istrkgb |
⊢ ( 𝐺 ∈ TarskiGB ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) ) |
19 |
18
|
simprbi |
⊢ ( 𝐺 ∈ TarskiGB → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃 ∀ 𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) |
20 |
19
|
simp2d |
⊢ ( 𝐺 ∈ TarskiGB → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ) |
21 |
17 20
|
syl |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ) |
22 |
|
oveq1 |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑧 ) ) |
23 |
22
|
eleq2d |
⊢ ( 𝑥 = 𝑋 → ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ↔ 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ) ) |
24 |
23
|
anbi1d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) ↔ ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) ) ) |
25 |
|
oveq2 |
⊢ ( 𝑥 = 𝑋 → ( 𝑣 𝐼 𝑥 ) = ( 𝑣 𝐼 𝑋 ) ) |
26 |
25
|
eleq2d |
⊢ ( 𝑥 = 𝑋 → ( 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ↔ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) |
27 |
26
|
anbi2d |
⊢ ( 𝑥 = 𝑋 → ( ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ↔ ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) |
28 |
27
|
rexbidv |
⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) |
29 |
24 28
|
imbi12d |
⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) ) |
30 |
29
|
2ralbidv |
⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) ) |
31 |
|
oveq1 |
⊢ ( 𝑦 = 𝑌 → ( 𝑦 𝐼 𝑧 ) = ( 𝑌 𝐼 𝑧 ) ) |
32 |
31
|
eleq2d |
⊢ ( 𝑦 = 𝑌 → ( 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ↔ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) ) |
33 |
32
|
anbi2d |
⊢ ( 𝑦 = 𝑌 → ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) ↔ ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) ) ) |
34 |
|
oveq2 |
⊢ ( 𝑦 = 𝑌 → ( 𝑢 𝐼 𝑦 ) = ( 𝑢 𝐼 𝑌 ) ) |
35 |
34
|
eleq2d |
⊢ ( 𝑦 = 𝑌 → ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ↔ 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ) ) |
36 |
35
|
anbi1d |
⊢ ( 𝑦 = 𝑌 → ( ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ↔ ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) |
37 |
36
|
rexbidv |
⊢ ( 𝑦 = 𝑌 → ( ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) |
38 |
33 37
|
imbi12d |
⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) ) |
39 |
38
|
2ralbidv |
⊢ ( 𝑦 = 𝑌 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) ) |
40 |
|
oveq2 |
⊢ ( 𝑧 = 𝑍 → ( 𝑋 𝐼 𝑧 ) = ( 𝑋 𝐼 𝑍 ) ) |
41 |
40
|
eleq2d |
⊢ ( 𝑧 = 𝑍 → ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ↔ 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ) ) |
42 |
|
oveq2 |
⊢ ( 𝑧 = 𝑍 → ( 𝑌 𝐼 𝑧 ) = ( 𝑌 𝐼 𝑍 ) ) |
43 |
42
|
eleq2d |
⊢ ( 𝑧 = 𝑍 → ( 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ↔ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) ) |
44 |
41 43
|
anbi12d |
⊢ ( 𝑧 = 𝑍 → ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) ↔ ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) ) ) |
45 |
44
|
imbi1d |
⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ↔ ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) ) |
46 |
45
|
2ralbidv |
⊢ ( 𝑧 = 𝑍 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ↔ ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) ) |
47 |
30 39 46
|
rspc3v |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) ) |
48 |
5 6 7 47
|
syl3anc |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) ) |
49 |
21 48
|
mpd |
⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) |
50 |
|
eleq1 |
⊢ ( 𝑢 = 𝑈 → ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ↔ 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ) ) |
51 |
50
|
anbi1d |
⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) ↔ ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) ) ) |
52 |
|
oveq1 |
⊢ ( 𝑢 = 𝑈 → ( 𝑢 𝐼 𝑌 ) = ( 𝑈 𝐼 𝑌 ) ) |
53 |
52
|
eleq2d |
⊢ ( 𝑢 = 𝑈 → ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ↔ 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ) ) |
54 |
53
|
anbi1d |
⊢ ( 𝑢 = 𝑈 → ( ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ↔ ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) |
55 |
54
|
rexbidv |
⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) |
56 |
51 55
|
imbi12d |
⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ↔ ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ) ) |
57 |
|
eleq1 |
⊢ ( 𝑣 = 𝑉 → ( 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ↔ 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) ) |
58 |
57
|
anbi2d |
⊢ ( 𝑣 = 𝑉 → ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) ↔ ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) ) ) |
59 |
|
oveq1 |
⊢ ( 𝑣 = 𝑉 → ( 𝑣 𝐼 𝑋 ) = ( 𝑉 𝐼 𝑋 ) ) |
60 |
59
|
eleq2d |
⊢ ( 𝑣 = 𝑉 → ( 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ↔ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) |
61 |
60
|
anbi2d |
⊢ ( 𝑣 = 𝑉 → ( ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ↔ ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) ) |
62 |
61
|
rexbidv |
⊢ ( 𝑣 = 𝑉 → ( ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ↔ ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) ) |
63 |
58 62
|
imbi12d |
⊢ ( 𝑣 = 𝑉 → ( ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) ↔ ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) ) ) |
64 |
56 63
|
rspc2v |
⊢ ( ( 𝑈 ∈ 𝑃 ∧ 𝑉 ∈ 𝑃 ) → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) → ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) ) ) |
65 |
8 9 64
|
syl2anc |
⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝑃 ∀ 𝑣 ∈ 𝑃 ( ( 𝑢 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑣 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑋 ) ) ) → ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) ) ) |
66 |
49 65
|
mpd |
⊢ ( 𝜑 → ( ( 𝑈 ∈ ( 𝑋 𝐼 𝑍 ) ∧ 𝑉 ∈ ( 𝑌 𝐼 𝑍 ) ) → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) ) |
67 |
10 11 66
|
mp2and |
⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ( 𝑎 ∈ ( 𝑈 𝐼 𝑌 ) ∧ 𝑎 ∈ ( 𝑉 𝐼 𝑋 ) ) ) |