This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opsrval

Description: The value of the "ordered power series" function. This is the same as mPwSer psrval , but with the addition of a well-order on I we can turn a strict order on R into a strict order on the power series structure. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses opsrval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
opsrval.o ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
opsrval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
opsrval.q ⊢ < = ( lt ‘ 𝑅 )
opsrval.c ⊢ 𝐶 = ( 𝑇 <bag 𝐼 )
opsrval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
opsrval.l ⊢ ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) }
opsrval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
opsrval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
opsrval.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
Assertion opsrval ( 𝜑 → 𝑂 = ( 𝑆 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )

Proof

Step Hyp Ref Expression
1 opsrval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 opsrval.o ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
3 opsrval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 opsrval.q ⊢ < = ( lt ‘ 𝑅 )
5 opsrval.c ⊢ 𝐶 = ( 𝑇 <bag 𝐼 )
6 opsrval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
7 opsrval.l ⊢ ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) }
8 opsrval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
9 opsrval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
10 opsrval.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
11 8 elexd ⊢ ( 𝜑 → 𝐼 ∈ V )
12 9 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
13 8 8 xpexd ⊢ ( 𝜑 → ( 𝐼 × 𝐼 ) ∈ V )
14 pwexg ⊢ ( ( 𝐼 × 𝐼 ) ∈ V → 𝒫 ( 𝐼 × 𝐼 ) ∈ V )
15 mptexg ⊢ ( 𝒫 ( 𝐼 × 𝐼 ) ∈ V → ( 𝑟 ∈ 𝒫 ( 𝐼 × 𝐼 ) ↦ ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) ∈ V )
16 13 14 15 3syl ⊢ ( 𝜑 → ( 𝑟 ∈ 𝒫 ( 𝐼 × 𝐼 ) ↦ ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) ∈ V )
17 simpl ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) → 𝑖 = 𝐼 )
18 17 sqxpeqd ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) → ( 𝑖 × 𝑖 ) = ( 𝐼 × 𝐼 ) )
19 18 pweqd ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) → 𝒫 ( 𝑖 × 𝑖 ) = 𝒫 ( 𝐼 × 𝐼 ) )
20 ovexd ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) → ( 𝑖 mPwSer 𝑠 ) ∈ V )
21 id ⊢ ( 𝑝 = ( 𝑖 mPwSer 𝑠 ) → 𝑝 = ( 𝑖 mPwSer 𝑠 ) )
22 oveq12 ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) → ( 𝑖 mPwSer 𝑠 ) = ( 𝐼 mPwSer 𝑅 ) )
23 21 22 sylan9eqr ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → 𝑝 = ( 𝐼 mPwSer 𝑅 ) )
24 23 1 eqtr4di ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → 𝑝 = 𝑆 )
25 24 fveq2d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → ( Base ‘ 𝑝 ) = ( Base ‘ 𝑆 ) )
26 25 3 eqtr4di ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → ( Base ‘ 𝑝 ) = 𝐵 )
27 26 sseq2d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐵 ) )
28 ovex ⊢ ( ℕ0 ↑m 𝑖 ) ∈ V
29 28 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V
30 29 a1i ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V )
31 17 adantr ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → 𝑖 = 𝐼 )
32 31 oveq2d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) )
33 rabeq ⊢ ( ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
34 32 33 syl ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
35 34 6 eqtr4di ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = 𝐷 )
36 simpr ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
37 simpllr ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) ∧ 𝑑 = 𝐷 ) → 𝑠 = 𝑅 )
38 37 fveq2d ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) ∧ 𝑑 = 𝐷 ) → ( lt ‘ 𝑠 ) = ( lt ‘ 𝑅 ) )
39 38 4 eqtr4di ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) ∧ 𝑑 = 𝐷 ) → ( lt ‘ 𝑠 ) = < )
40 39 breqd ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) ∧ 𝑑 = 𝐷 ) → ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ↔ ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ) )
41 31 adantr ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) ∧ 𝑑 = 𝐷 ) → 𝑖 = 𝐼 )
42 41 oveq2d ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) ∧ 𝑑 = 𝐷 ) → ( 𝑟 <bag 𝑖 ) = ( 𝑟 <bag 𝐼 ) )
43 42 breqd ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) ∧ 𝑑 = 𝐷 ) → ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 ↔ 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 ) )
44 43 imbi1d ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) ∧ 𝑑 = 𝐷 ) → ( ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
45 36 44 raleqbidv ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) ∧ 𝑑 = 𝐷 ) → ( ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
46 40 45 anbi12d ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) ∧ 𝑑 = 𝐷 ) → ( ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
47 36 46 rexeqbidv ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) ∧ 𝑑 = 𝐷 ) → ( ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
48 30 35 47 sbcied2 ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
49 48 orbi1d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → ( ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ↔ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) )
50 27 49 anbi12d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → ( ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) ) )
51 50 opabbidv ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } )
52 51 opeq2d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ = ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ )
53 24 52 oveq12d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) ∧ 𝑝 = ( 𝑖 mPwSer 𝑠 ) ) → ( 𝑝 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) = ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) )
54 20 53 csbied ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) → ⦋ ( 𝑖 mPwSer 𝑠 ) / 𝑝 ⦌ ( 𝑝 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) = ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) )
55 19 54 mpteq12dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑅 ) → ( 𝑟 ∈ 𝒫 ( 𝑖 × 𝑖 ) ↦ ⦋ ( 𝑖 mPwSer 𝑠 ) / 𝑝 ⦌ ( 𝑝 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) = ( 𝑟 ∈ 𝒫 ( 𝐼 × 𝐼 ) ↦ ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) )
56 df-opsr ⊢ ordPwSer = ( 𝑖 ∈ V , 𝑠 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑖 × 𝑖 ) ↦ ⦋ ( 𝑖 mPwSer 𝑠 ) / 𝑝 ⦌ ( 𝑝 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) )
57 55 56 ovmpoga ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ∧ ( 𝑟 ∈ 𝒫 ( 𝐼 × 𝐼 ) ↦ ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) ∈ V ) → ( 𝐼 ordPwSer 𝑅 ) = ( 𝑟 ∈ 𝒫 ( 𝐼 × 𝐼 ) ↦ ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) )
58 11 12 16 57 syl3anc ⊢ ( 𝜑 → ( 𝐼 ordPwSer 𝑅 ) = ( 𝑟 ∈ 𝒫 ( 𝐼 × 𝐼 ) ↦ ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) )
59 simpr ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → 𝑟 = 𝑇 )
60 59 oveq1d ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → ( 𝑟 <bag 𝐼 ) = ( 𝑇 <bag 𝐼 ) )
61 60 5 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → ( 𝑟 <bag 𝐼 ) = 𝐶 )
62 61 breqd ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 ↔ 𝑤 𝐶 𝑧 ) )
63 62 imbi1d ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → ( ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
64 63 ralbidv ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → ( ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
65 64 anbi2d ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → ( ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
66 65 rexbidv ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
67 66 orbi1d ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → ( ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ↔ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) )
68 67 anbi2d ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → ( ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) ) )
69 68 opabbidv ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 𝐶 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } )
70 69 7 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = ≤ )
71 70 opeq2d ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ = ⟨ ( le ‘ ndx ) , ≤ ⟩ )
72 71 oveq2d ⊢ ( ( 𝜑 ∧ 𝑟 = 𝑇 ) → ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ∃ 𝑧 ∈ 𝐷 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐷 ( 𝑤 ( 𝑟 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) = ( 𝑆 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )
73 13 10 sselpwd ⊢ ( 𝜑 → 𝑇 ∈ 𝒫 ( 𝐼 × 𝐼 ) )
74 ovexd ⊢ ( 𝜑 → ( 𝑆 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) ∈ V )
75 58 72 73 74 fvmptd ⊢ ( 𝜑 → ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 ) = ( 𝑆 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )
76 2 75 eqtrid ⊢ ( 𝜑 → 𝑂 = ( 𝑆 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )