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 } ∧ ∃ 𝑧 ∈ 𝑖 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } )