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

Metamath Proof Explorer

Definition df-ltbag

Description: Define a well-order on the set of all finite bags from the index set i given a wellordering r of i . (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Assertion df-ltbag <bag = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ ∃ 𝑧 ∈ 𝑖 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cltb ⊢ <bag
1 vr ⊢ 𝑟
2 cvv ⊢ V
3 vi ⊢ 𝑖
4 vx ⊢ 𝑥
5 vy ⊢ 𝑦
6 4 cv ⊢ 𝑥
7 5 cv ⊢ 𝑦
8 6 7 cpr ⊢ { 𝑥 , 𝑦 }
9 vh ⊢ ℎ
10 cn0 ⊢ ℕ0
11 cmap ⊢ ↑m
12 3 cv ⊢ 𝑖
13 10 12 11 co ⊢ ( ℕ0 ↑m 𝑖 )
14 9 cv ⊢ ℎ
15 14 ccnv ⊢ ◡ ℎ
16 cn ⊢ ℕ
17 15 16 cima ⊢ ( ◡ ℎ “ ℕ )
18 cfn ⊢ Fin
19 17 18 wcel ⊢ ( ◡ ℎ “ ℕ ) ∈ Fin
20 19 9 13 crab ⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
21 8 20 wss ⊢ { 𝑥 , 𝑦 } ⊆ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
22 vz ⊢ 𝑧
23 22 cv ⊢ 𝑧
24 23 6 cfv ⊢ ( 𝑥 ‘ 𝑧 )
25 clt ⊢ <
26 23 7 cfv ⊢ ( 𝑦 ‘ 𝑧 )
27 24 26 25 wbr ⊢ ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 )
28 vw ⊢ 𝑤
29 1 cv ⊢ 𝑟
30 28 cv ⊢ 𝑤
31 23 30 29 wbr ⊢ 𝑧 𝑟 𝑤
32 30 6 cfv ⊢ ( 𝑥 ‘ 𝑤 )
33 30 7 cfv ⊢ ( 𝑦 ‘ 𝑤 )
34 32 33 wceq ⊢ ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 )
35 31 34 wi ⊢ ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) )
36 35 28 12 wral ⊢ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) )
37 27 36 wa ⊢ ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) )
38 37 22 12 wrex ⊢ ∃ 𝑧 ∈ 𝑖 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) )
39 21 38 wa ⊢ ( { 𝑥 , 𝑦 } ⊆ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ ∃ 𝑧 ∈ 𝑖 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
40 39 4 5 copab ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ ∃ 𝑧 ∈ 𝑖 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) }
41 1 3 2 2 40 cmpo ⊢ ( 𝑟 ∈ V , 𝑖 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ ∃ 𝑧 ∈ 𝑖 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } )
42 0 41 wceq ⊢ <bag = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ ∃ 𝑧 ∈ 𝑖 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } )