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

Metamath Proof Explorer

Theorem ltbwe

Description: The finite bag order is a well-order, given a well-order of the index set. (Contributed by Mario Carneiro, 2-Jun-2015)

Ref Expression
Hypotheses ltbval.c ⊢ 𝐶 = ( 𝑇 <bag 𝐼 )
ltbval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
ltbval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
ltbval.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑊 )
ltbwe.w ⊢ ( 𝜑 → 𝑇 We 𝐼 )
Assertion ltbwe ( 𝜑 → 𝐶 We 𝐷 )

Proof

Step Hyp Ref Expression
1 ltbval.c ⊢ 𝐶 = ( 𝑇 <bag 𝐼 )
2 ltbval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
3 ltbval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 ltbval.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑊 )
5 ltbwe.w ⊢ ( 𝜑 → 𝑇 We 𝐼 )
6 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
7 breq1 ⊢ ( ℎ = 𝑥 → ( ℎ finSupp 0 ↔ 𝑥 finSupp 0 ) )
8 7 cbvrabv ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { 𝑥 ∈ ( ℕ0 ↑m 𝐼 ) ∣ 𝑥 finSupp 0 }
9 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
10 ltweuz ⊢ < We ( ℤ≥ ‘ 0 )
11 weeq2 ⊢ ( ℕ0 = ( ℤ≥ ‘ 0 ) → ( < We ℕ0 ↔ < We ( ℤ≥ ‘ 0 ) ) )
12 10 11 mpbiri ⊢ ( ℕ0 = ( ℤ≥ ‘ 0 ) → < We ℕ0 )
13 9 12 mp1i ⊢ ( 𝜑 → < We ℕ0 )
14 0nn0 ⊢ 0 ∈ ℕ0
15 ne0i ⊢ ( 0 ∈ ℕ0 → ℕ0 ≠ ∅ )
16 14 15 mp1i ⊢ ( 𝜑 → ℕ0 ≠ ∅ )
17 eqid ⊢ OrdIso ( 𝑇 , 𝐼 ) = OrdIso ( 𝑇 , 𝐼 )
18 0z ⊢ 0 ∈ ℤ
19 hashgval2 ⊢ ( ♯ ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
20 18 19 om2uzoi ⊢ ( ♯ ↾ ω ) = OrdIso ( < , ( ℤ≥ ‘ 0 ) )
21 oieq2 ⊢ ( ℕ0 = ( ℤ≥ ‘ 0 ) → OrdIso ( < , ℕ0 ) = OrdIso ( < , ( ℤ≥ ‘ 0 ) ) )
22 9 21 ax-mp ⊢ OrdIso ( < , ℕ0 ) = OrdIso ( < , ( ℤ≥ ‘ 0 ) )
23 20 22 eqtr4i ⊢ ( ♯ ↾ ω ) = OrdIso ( < , ℕ0 )
24 peano1 ⊢ ∅ ∈ ω
25 fvres ⊢ ( ∅ ∈ ω → ( ( ♯ ↾ ω ) ‘ ∅ ) = ( ♯ ‘ ∅ ) )
26 24 25 ax-mp ⊢ ( ( ♯ ↾ ω ) ‘ ∅ ) = ( ♯ ‘ ∅ )
27 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
28 26 27 eqtr2i ⊢ 0 = ( ( ♯ ↾ ω ) ‘ ∅ )
29 6 8 5 13 16 17 23 28 wemapwe ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } We { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
30 elmapfun ⊢ ( ℎ ∈ ( ℕ0 ↑m 𝐼 ) → Fun ℎ )
31 30 adantl ⊢ ( ( 𝜑 ∧ ℎ ∈ ( ℕ0 ↑m 𝐼 ) ) → Fun ℎ )
32 simpr ⊢ ( ( 𝜑 ∧ ℎ ∈ ( ℕ0 ↑m 𝐼 ) ) → ℎ ∈ ( ℕ0 ↑m 𝐼 ) )
33 c0ex ⊢ 0 ∈ V
34 33 a1i ⊢ ( ( 𝜑 ∧ ℎ ∈ ( ℕ0 ↑m 𝐼 ) ) → 0 ∈ V )
35 funisfsupp ⊢ ( ( Fun ℎ ∧ ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∧ 0 ∈ V ) → ( ℎ finSupp 0 ↔ ( ℎ supp 0 ) ∈ Fin ) )
36 31 32 34 35 syl3anc ⊢ ( ( 𝜑 ∧ ℎ ∈ ( ℕ0 ↑m 𝐼 ) ) → ( ℎ finSupp 0 ↔ ( ℎ supp 0 ) ∈ Fin ) )
37 elmapi ⊢ ( ℎ ∈ ( ℕ0 ↑m 𝐼 ) → ℎ : 𝐼 ⟶ ℕ0 )
38 fcdmnn0supp ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ℎ : 𝐼 ⟶ ℕ0 ) → ( ℎ supp 0 ) = ( ◡ ℎ “ ℕ ) )
39 38 eleq1d ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ℎ : 𝐼 ⟶ ℕ0 ) → ( ( ℎ supp 0 ) ∈ Fin ↔ ( ◡ ℎ “ ℕ ) ∈ Fin ) )
40 3 37 39 syl2an ⊢ ( ( 𝜑 ∧ ℎ ∈ ( ℕ0 ↑m 𝐼 ) ) → ( ( ℎ supp 0 ) ∈ Fin ↔ ( ◡ ℎ “ ℕ ) ∈ Fin ) )
41 36 40 bitr2d ⊢ ( ( 𝜑 ∧ ℎ ∈ ( ℕ0 ↑m 𝐼 ) ) → ( ( ◡ ℎ “ ℕ ) ∈ Fin ↔ ℎ finSupp 0 ) )
42 41 rabbidva ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
43 2 42 eqtrid ⊢ ( 𝜑 → 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } )
44 weeq2 ⊢ ( 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } We 𝐷 ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } We { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) )
45 43 44 syl ⊢ ( 𝜑 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } We 𝐷 ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } We { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } ) )
46 29 45 mpbird ⊢ ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } We 𝐷 )
47 weinxp ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } We 𝐷 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ ( 𝐷 × 𝐷 ) ) We 𝐷 )
48 46 47 sylib ⊢ ( 𝜑 → ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ ( 𝐷 × 𝐷 ) ) We 𝐷 )
49 1 2 3 4 ltbval ⊢ ( 𝜑 → 𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } )
50 df-xp ⊢ ( 𝐷 × 𝐷 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) }
51 vex ⊢ 𝑥 ∈ V
52 vex ⊢ 𝑦 ∈ V
53 51 52 prss ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐷 )
54 53 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ⊆ 𝐷 }
55 50 54 eqtr2i ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ⊆ 𝐷 } = ( 𝐷 × 𝐷 )
56 55 ineq1i ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ⊆ 𝐷 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ) = ( ( 𝐷 × 𝐷 ) ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } )
57 inopab ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ⊆ 𝐷 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) }
58 incom ⊢ ( ( 𝐷 × 𝐷 ) ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ) = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ ( 𝐷 × 𝐷 ) )
59 56 57 58 3eqtr3i ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ) } = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ ( 𝐷 × 𝐷 ) )
60 49 59 eqtrdi ⊢ ( 𝜑 → 𝐶 = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ ( 𝐷 × 𝐷 ) ) )
61 weeq1 ⊢ ( 𝐶 = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ ( 𝐷 × 𝐷 ) ) → ( 𝐶 We 𝐷 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ ( 𝐷 × 𝐷 ) ) We 𝐷 ) )
62 60 61 syl ⊢ ( 𝜑 → ( 𝐶 We 𝐷 ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐼 ( ( 𝑥 ‘ 𝑧 ) < ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐼 ( 𝑧 𝑇 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } ∩ ( 𝐷 × 𝐷 ) ) We 𝐷 ) )
63 48 62 mpbird ⊢ ( 𝜑 → 𝐶 We 𝐷 )