infxpen

Description: Every infinite ordinal is equinumerous to its Cartesian square. Proposition 10.39 of TakeutiZaring p. 94, whose proof we follow closely. The key idea is to show that the relation R is a well-ordering of ( On X. On ) with the additional property that R -initial segments of ( x X. x ) (where x is a limit ordinal) are of cardinality at most x . (Contributed by Mario Carneiro, 9-Mar-2013) (Revised by Mario Carneiro, 26-Jun-2015)

		Ref	Expression
	Assertion	infxpen	$⊢ (A \in On \land ω \subseteq A) \to (A \times A) \approx A$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} = \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\}$
2		eleq1w	$⊢ s = z \to (s \in (On \times On) \leftrightarrow z \in (On \times On))$
3		eleq1w	$⊢ t = w \to (t \in (On \times On) \leftrightarrow w \in (On \times On))$
4	2 3	bi2anan9	$⊢ (s = z \land t = w) \to ((s \in (On \times On) \land t \in (On \times On)) \leftrightarrow (z \in (On \times On) \land w \in (On \times On)))$
5		fveq2	$⊢ s = z \to 1^{st} (s) = 1^{st} (z)$
6		fveq2	$⊢ s = z \to 2^{nd} (s) = 2^{nd} (z)$
7	5 6	uneq12d	$⊢ s = z \to 1^{st} (s) \cup 2^{nd} (s) = 1^{st} (z) \cup 2^{nd} (z)$
8	7	adantr	$⊢ (s = z \land t = w) \to 1^{st} (s) \cup 2^{nd} (s) = 1^{st} (z) \cup 2^{nd} (z)$
9		fveq2	$⊢ t = w \to 1^{st} (t) = 1^{st} (w)$
10		fveq2	$⊢ t = w \to 2^{nd} (t) = 2^{nd} (w)$
11	9 10	uneq12d	$⊢ t = w \to 1^{st} (t) \cup 2^{nd} (t) = 1^{st} (w) \cup 2^{nd} (w)$
12	11	adantl	$⊢ (s = z \land t = w) \to 1^{st} (t) \cup 2^{nd} (t) = 1^{st} (w) \cup 2^{nd} (w)$
13	8 12	eleq12d	$⊢ (s = z \land t = w) \to (1^{st} (s) \cup 2^{nd} (s) \in (1^{st} (t) \cup 2^{nd} (t)) \leftrightarrow 1^{st} (z) \cup 2^{nd} (z) \in (1^{st} (w) \cup 2^{nd} (w)))$
14	7 11	eqeqan12d	$⊢ (s = z \land t = w) \to (1^{st} (s) \cup 2^{nd} (s) = 1^{st} (t) \cup 2^{nd} (t) \leftrightarrow 1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w))$
15		breq12	$⊢ (s = z \land t = w) \to (s \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} t \leftrightarrow z \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} w)$
16	14 15	anbi12d	$⊢ (s = z \land t = w) \to ((1^{st} (s) \cup 2^{nd} (s) = 1^{st} (t) \cup 2^{nd} (t) \land s \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} t) \leftrightarrow (1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w) \land z \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} w))$
17	13 16	orbi12d	$⊢ (s = z \land t = w) \to ((1^{st} (s) \cup 2^{nd} (s) \in (1^{st} (t) \cup 2^{nd} (t)) \lor (1^{st} (s) \cup 2^{nd} (s) = 1^{st} (t) \cup 2^{nd} (t) \land s \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} t)) \leftrightarrow (1^{st} (z) \cup 2^{nd} (z) \in (1^{st} (w) \cup 2^{nd} (w)) \lor (1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w) \land z \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} w)))$
18	4 17	anbi12d	$⊢ (s = z \land t = w) \to (((s \in (On \times On) \land t \in (On \times On)) \land (1^{st} (s) \cup 2^{nd} (s) \in (1^{st} (t) \cup 2^{nd} (t)) \lor (1^{st} (s) \cup 2^{nd} (s) = 1^{st} (t) \cup 2^{nd} (t) \land s \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} t))) \leftrightarrow ((z \in (On \times On) \land w \in (On \times On)) \land (1^{st} (z) \cup 2^{nd} (z) \in (1^{st} (w) \cup 2^{nd} (w)) \lor (1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w) \land z \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} w))))$
19	18	cbvopabv	$⊢ \{⟨s, t⟩ \| ((s \in (On \times On) \land t \in (On \times On)) \land (1^{st} (s) \cup 2^{nd} (s) \in (1^{st} (t) \cup 2^{nd} (t)) \lor (1^{st} (s) \cup 2^{nd} (s) = 1^{st} (t) \cup 2^{nd} (t) \land s \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} t)))\} = \{⟨z, w⟩ \| ((z \in (On \times On) \land w \in (On \times On)) \land (1^{st} (z) \cup 2^{nd} (z) \in (1^{st} (w) \cup 2^{nd} (w)) \lor (1^{st} (z) \cup 2^{nd} (z) = 1^{st} (w) \cup 2^{nd} (w) \land z \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} w)))\}$
20		eqid	$⊢ \{⟨s, t⟩ \| ((s \in (On \times On) \land t \in (On \times On)) \land (1^{st} (s) \cup 2^{nd} (s) \in (1^{st} (t) \cup 2^{nd} (t)) \lor (1^{st} (s) \cup 2^{nd} (s) = 1^{st} (t) \cup 2^{nd} (t) \land s \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} t)))\} \cap ((a \times a) \times (a \times a)) = \{⟨s, t⟩ \| ((s \in (On \times On) \land t \in (On \times On)) \land (1^{st} (s) \cup 2^{nd} (s) \in (1^{st} (t) \cup 2^{nd} (t)) \lor (1^{st} (s) \cup 2^{nd} (s) = 1^{st} (t) \cup 2^{nd} (t) \land s \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} t)))\} \cap ((a \times a) \times (a \times a))$
21		biid	$⊢ ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \forall m \in a m ≺ a)) \leftrightarrow ((a \in On \land \forall m \in a (ω \subseteq m \to (m \times m) \approx m)) \land (ω \subseteq a \land \forall m \in a m ≺ a))$
22		eqid	$⊢ 1^{st} (w) \cup 2^{nd} (w) = 1^{st} (w) \cup 2^{nd} (w)$
23		eqid	$⊢ OrdIso (\{⟨s, t⟩ \| ((s \in (On \times On) \land t \in (On \times On)) \land (1^{st} (s) \cup 2^{nd} (s) \in (1^{st} (t) \cup 2^{nd} (t)) \lor (1^{st} (s) \cup 2^{nd} (s) = 1^{st} (t) \cup 2^{nd} (t) \land s \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} t)))\} \cap ((a \times a) \times (a \times a)), a \times a) = OrdIso (\{⟨s, t⟩ \| ((s \in (On \times On) \land t \in (On \times On)) \land (1^{st} (s) \cup 2^{nd} (s) \in (1^{st} (t) \cup 2^{nd} (t)) \lor (1^{st} (s) \cup 2^{nd} (s) = 1^{st} (t) \cup 2^{nd} (t) \land s \{⟨x, y⟩ \| ((x \in (On \times On) \land y \in (On \times On)) \land (1^{st} (x) \in 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) \in 2^{nd} (y))))\} t)))\} \cap ((a \times a) \times (a \times a)), a \times a)$
24	1 19 20 21 22 23	infxpenlem	$⊢ (A \in On \land ω \subseteq A) \to (A \times A) \approx A$

Metamath Proof Explorer

Theorem infxpen

Proof