ltweuz

Description: < is a well-founded relation on any sequence of upper integers. (Contributed by Andrew Salmon, 13-Nov-2011) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	ltweuz	$⊢ < We ℤ_{\geq A}$

Proof

Step	Hyp	Ref	Expression
1		ordom	$⊢ Ord ω$
2		ordwe	$⊢ Ord ω \to E We ω$
3	1 2	ax-mp	$⊢ E We ω$
4		rdgeq2	$⊢ A = if (A \in ℤ, A, 0) \to rec ((x \in V ⟼ x + 1), A) = rec ((x \in V ⟼ x + 1), if (A \in ℤ, A, 0))$
5	4	reseq1d	$⊢ A = if (A \in ℤ, A, 0) \to {rec ((x \in V ⟼ x + 1), A) ↾}_{ω} = {rec ((x \in V ⟼ x + 1), if (A \in ℤ, A, 0)) ↾}_{ω}$
6		isoeq1	$⊢ {rec ((x \in V ⟼ x + 1), A) ↾}_{ω} = {rec ((x \in V ⟼ x + 1), if (A \in ℤ, A, 0)) ↾}_{ω} \to (({rec ((x \in V ⟼ x + 1), A) ↾}_{ω}) {Isom}_{E, <} (ω, ℤ_{\geq A}) \leftrightarrow ({rec ((x \in V ⟼ x + 1), if (A \in ℤ, A, 0)) ↾}_{ω}) {Isom}_{E, <} (ω, ℤ_{\geq A}))$
7	5 6	syl	$⊢ A = if (A \in ℤ, A, 0) \to (({rec ((x \in V ⟼ x + 1), A) ↾}_{ω}) {Isom}_{E, <} (ω, ℤ_{\geq A}) \leftrightarrow ({rec ((x \in V ⟼ x + 1), if (A \in ℤ, A, 0)) ↾}_{ω}) {Isom}_{E, <} (ω, ℤ_{\geq A}))$
8		fveq2	$⊢ A = if (A \in ℤ, A, 0) \to ℤ_{\geq A} = ℤ_{\geq if (A \in ℤ, A, 0)}$
9		isoeq5	$⊢ ℤ_{\geq A} = ℤ_{\geq if (A \in ℤ, A, 0)} \to (({rec ((x \in V ⟼ x + 1), if (A \in ℤ, A, 0)) ↾}_{ω}) {Isom}_{E, <} (ω, ℤ_{\geq A}) \leftrightarrow ({rec ((x \in V ⟼ x + 1), if (A \in ℤ, A, 0)) ↾}_{ω}) {Isom}_{E, <} (ω, ℤ_{\geq if (A \in ℤ, A, 0)}))$
10	8 9	syl	$⊢ A = if (A \in ℤ, A, 0) \to (({rec ((x \in V ⟼ x + 1), if (A \in ℤ, A, 0)) ↾}_{ω}) {Isom}_{E, <} (ω, ℤ_{\geq A}) \leftrightarrow ({rec ((x \in V ⟼ x + 1), if (A \in ℤ, A, 0)) ↾}_{ω}) {Isom}_{E, <} (ω, ℤ_{\geq if (A \in ℤ, A, 0)}))$
11		0z	$⊢ 0 \in ℤ$
12	11	elimel	$⊢ if (A \in ℤ, A, 0) \in ℤ$
13		eqid	$⊢ {rec ((x \in V ⟼ x + 1), if (A \in ℤ, A, 0)) ↾}_{ω} = {rec ((x \in V ⟼ x + 1), if (A \in ℤ, A, 0)) ↾}_{ω}$
14	12 13	om2uzisoi	$⊢ ({rec ((x \in V ⟼ x + 1), if (A \in ℤ, A, 0)) ↾}_{ω}) {Isom}_{E, <} (ω, ℤ_{\geq if (A \in ℤ, A, 0)})$
15	7 10 14	dedth2v	$⊢ A \in ℤ \to ({rec ((x \in V ⟼ x + 1), A) ↾}_{ω}) {Isom}_{E, <} (ω, ℤ_{\geq A})$
16		isocnv	$⊢ ({rec ((x \in V ⟼ x + 1), A) ↾}_{ω}) {Isom}_{E, <} (ω, ℤ_{\geq A}) \to {({rec ((x \in V ⟼ x + 1), A) ↾}_{ω})}^{-1} {Isom}_{<, E} (ℤ_{\geq A}, ω)$
17	15 16	syl	$⊢ A \in ℤ \to {({rec ((x \in V ⟼ x + 1), A) ↾}_{ω})}^{-1} {Isom}_{<, E} (ℤ_{\geq A}, ω)$
18		dmres	$⊢ dom ({rec ((x \in V ⟼ x + 1), A) ↾}_{ω}) = ω \cap dom rec ((x \in V ⟼ x + 1), A)$
19		omex	$⊢ ω \in V$
20	19	inex1	$⊢ ω \cap dom rec ((x \in V ⟼ x + 1), A) \in V$
21	18 20	eqeltri	$⊢ dom ({rec ((x \in V ⟼ x + 1), A) ↾}_{ω}) \in V$
22		cnvimass	$⊢ {({rec ((x \in V ⟼ x + 1), A) ↾}_{ω})}^{-1} [y] \subseteq dom ({rec ((x \in V ⟼ x + 1), A) ↾}_{ω})$
23	21 22	ssexi	$⊢ {({rec ((x \in V ⟼ x + 1), A) ↾}_{ω})}^{-1} [y] \in V$
24	23	ax-gen	$⊢ \forall y {({rec ((x \in V ⟼ x + 1), A) ↾}_{ω})}^{-1} [y] \in V$
25		isowe2	$⊢ ({({rec ((x \in V ⟼ x + 1), A) ↾}_{ω})}^{-1} {Isom}_{<, E} (ℤ_{\geq A}, ω) \land \forall y {({rec ((x \in V ⟼ x + 1), A) ↾}_{ω})}^{-1} [y] \in V) \to (E We ω \to < We ℤ_{\geq A})$
26	17 24 25	sylancl	$⊢ A \in ℤ \to (E We ω \to < We ℤ_{\geq A})$
27	3 26	mpi	$⊢ A \in ℤ \to < We ℤ_{\geq A}$
28		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
29	28	fdmi	$⊢ dom ℤ_{\geq} = ℤ$
30	27 29	eleq2s	$⊢ A \in dom ℤ_{\geq} \to < We ℤ_{\geq A}$
31		we0	$⊢ < We \emptyset$
32		ndmfv	$⊢ \neg A \in dom ℤ_{\geq} \to ℤ_{\geq A} = \emptyset$
33		weeq2	$⊢ ℤ_{\geq A} = \emptyset \to (< We ℤ_{\geq A} \leftrightarrow < We \emptyset)$
34	32 33	syl	$⊢ \neg A \in dom ℤ_{\geq} \to (< We ℤ_{\geq A} \leftrightarrow < We \emptyset)$
35	31 34	mpbiri	$⊢ \neg A \in dom ℤ_{\geq} \to < We ℤ_{\geq A}$
36	30 35	pm2.61i	$⊢ < We ℤ_{\geq A}$

Metamath Proof Explorer

Theorem ltweuz

Proof