Metamath Proof Explorer

Theorem oduprs

Description: Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018)

Ref Expression
Hypothesis oduprs.d ⊢ 𝐷 = ( ODual ‘ 𝐾 )
Assertion oduprs ( 𝐾 ∈ Proset → 𝐷 ∈ Proset )

Proof

Step Hyp Ref Expression
1 oduprs.d ⊢ 𝐷 = ( ODual ‘ 𝐾 )
2 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
3 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4 2 3 isprs ⊢ ( 𝐾 ∈ Proset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
5 4 simprbi ⊢ ( 𝐾 ∈ Proset → ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
6 5 r19.21bi ⊢ ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
7 6 r19.21bi ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
8 7 r19.21bi ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
9 8 simpld ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → 𝑥 ( le ‘ 𝐾 ) 𝑥 )
10 vex ⊢ 𝑥 ∈ V
11 10 10 brcnv ⊢ ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑥 ↔ 𝑥 ( le ‘ 𝐾 ) 𝑥 )
12 9 11 sylibr ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → 𝑥 ◡ ( le ‘ 𝐾 ) 𝑥 )
13 2 3 isprs ⊢ ( 𝐾 ∈ Proset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑧 ( le ‘ 𝐾 ) 𝑧 ∧ ( ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) )
14 13 simprbi ⊢ ( 𝐾 ∈ Proset → ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑧 ( le ‘ 𝐾 ) 𝑧 ∧ ( ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
15 14 r19.21bi ⊢ ( ( 𝐾 ∈ Proset ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑧 ( le ‘ 𝐾 ) 𝑧 ∧ ( ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
16 15 r19.21bi ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑧 ( le ‘ 𝐾 ) 𝑧 ∧ ( ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
17 16 r19.21bi ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑧 ( le ‘ 𝐾 ) 𝑧 ∧ ( ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
18 17 simprd ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) )
19 18 an32s ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) )
20 19 ex ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐾 ) → ( ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
21 20 an32s ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐾 ) → ( ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
22 21 imp ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) )
23 22 an32s ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) )
24 vex ⊢ 𝑦 ∈ V
25 10 24 brcnv ⊢ ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ↔ 𝑦 ( le ‘ 𝐾 ) 𝑥 )
26 vex ⊢ 𝑧 ∈ V
27 24 26 brcnv ⊢ ( 𝑦 ◡ ( le ‘ 𝐾 ) 𝑧 ↔ 𝑧 ( le ‘ 𝐾 ) 𝑦 )
28 25 27 anbi12ci ⊢ ( ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑧 ) ↔ ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) )
29 10 26 brcnv ⊢ ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑧 ↔ 𝑧 ( le ‘ 𝐾 ) 𝑥 )
30 23 28 29 3imtr4g ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ◡ ( le ‘ 𝐾 ) 𝑧 ) )
31 12 30 jca ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ◡ ( le ‘ 𝐾 ) 𝑧 ) ) )
32 31 ralrimiva ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ◡ ( le ‘ 𝐾 ) 𝑧 ) ) )
33 32 ralrimiva ⊢ ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ◡ ( le ‘ 𝐾 ) 𝑧 ) ) )
34 33 ralrimiva ⊢ ( 𝐾 ∈ Proset → ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ◡ ( le ‘ 𝐾 ) 𝑧 ) ) )
35 1 fvexi ⊢ 𝐷 ∈ V
36 34 35 jctil ⊢ ( 𝐾 ∈ Proset → ( 𝐷 ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ◡ ( le ‘ 𝐾 ) 𝑧 ) ) ) )
37 1 2 odubas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐷 )
38 1 3 oduleval ⊢ ◡ ( le ‘ 𝐾 ) = ( le ‘ 𝐷 )
39 37 38 isprs ⊢ ( 𝐷 ∈ Proset ↔ ( 𝐷 ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ◡ ( le ‘ 𝐾 ) 𝑧 ) ) ) )
40 36 39 sylibr ⊢ ( 𝐾 ∈ Proset → 𝐷 ∈ Proset )