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		frnnn0supp	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ℎ : 𝐼 ⟶ ℕ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 𝐷 )