Metamath Proof Explorer

Theorem ltbval

Description: Value of the well-order on finite bags. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses ltbval.c ⊢ 𝐶 = ( 𝑇 <bag 𝐼 )
ltbval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
ltbval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
ltbval.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑊 )
Assertion ltbval ( 𝜑 → 𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 ltbval.c ⊢ 𝐶 = ( 𝑇 <bag 𝐼 )
2 ltbval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
3 ltbval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 ltbval.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑊 )
5 elex ⊢ ( 𝑇 ∈ 𝑊 → 𝑇 ∈ V )
6 elex ⊢ ( 𝐼 ∈ 𝑉 → 𝐼 ∈ V )
7 simpr ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → 𝑖 = 𝐼 )
8 7 oveq2d ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) )
9 rabeq ⊢ ( ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
10 8 9 syl ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
11 10 2 eqtr4di ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = 𝐷 )
12 11 sseq2d ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → ( { 𝑥 , 𝑦 } ⊆ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↔ { 𝑥 , 𝑦 } ⊆ 𝐷 ) )
13 simpl ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → 𝑟 = 𝑇 )
14 13 breqd ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → ( 𝑧 𝑟 𝑤 ↔ 𝑧 𝑇 𝑤 ) )
15 14 imbi1d ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → ( ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
16 7 15 raleqbidv ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → ( ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
17 16 anbi2d ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → ( ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
18 7 17 rexeqbidv ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → ( ∃ 𝑧 ∈ 𝑖 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
19 12 18 anbi12d ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → ( ( { 𝑥 , 𝑦 } ⊆ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ ∃ 𝑧 ∈ 𝑖 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) ) )
20 19 opabbidv ⊢ ( ( 𝑟 = 𝑇 ∧ 𝑖 = 𝐼 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ ∃ 𝑧 ∈ 𝑖 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } )
21 df-ltbag ⊢ <bag = ( 𝑟 ∈ V , 𝑖 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∧ ∃ 𝑧 ∈ 𝑖 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑖 ( 𝑧 𝑟 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } )
22 vex ⊢ 𝑥 ∈ V
23 vex ⊢ 𝑦 ∈ V
24 22 23 prss ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐷 )
25 24 anbi1i ⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) )
26 25 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) }
27 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
28 2 27 rabex2 ⊢ 𝐷 ∈ V
29 28 28 xpex ⊢ ( 𝐷 × 𝐷 ) ∈ V
30 opabssxp ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } ⊆ ( 𝐷 × 𝐷 )
31 29 30 ssexi ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } ∈ V
32 26 31 eqeltrri ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } ∈ V
33 20 21 32 ovmpoa ⊢ ( ( 𝑇 ∈ V ∧ 𝐼 ∈ V ) → ( 𝑇 <bag 𝐼 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } )
34 5 6 33 syl2an ⊢ ( ( 𝑇 ∈ 𝑊 ∧ 𝐼 ∈ 𝑉 ) → ( 𝑇 <bag 𝐼 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } )
35 4 3 34 syl2anc ⊢ ( 𝜑 → ( 𝑇 <bag 𝐼 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } )
36 1 35 syl5eq ⊢ ( 𝜑 → 𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } )