oev2

Description: Alternate value of ordinal exponentiation. Compare oev . (Contributed by NM, 2-Jan-2004) (Revised by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Assertion	oev2	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ((V ∖ ⋂ A) \cup ⋂ B)$

Proof

Step	Hyp	Ref	Expression
1		oveq12	$⊢ (A = \emptyset \land B = \emptyset) \to A ↑_{𝑜} B = \emptyset ↑_{𝑜} \emptyset$
2		oe0m0	$⊢ \emptyset ↑_{𝑜} \emptyset = 1_{𝑜}$
3	1 2	eqtrdi	$⊢ (A = \emptyset \land B = \emptyset) \to A ↑_{𝑜} B = 1_{𝑜}$
4		fveq2	$⊢ B = \emptyset \to rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (\emptyset)$
5		1oex	$⊢ 1_{𝑜} \in V$
6	5	rdg0	$⊢ rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (\emptyset) = 1_{𝑜}$
7	4 6	eqtrdi	$⊢ B = \emptyset \to rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) = 1_{𝑜}$
8		inteq	$⊢ B = \emptyset \to ⋂ B = ⋂ \emptyset$
9		int0	$⊢ ⋂ \emptyset = V$
10	8 9	eqtrdi	$⊢ B = \emptyset \to ⋂ B = V$
11	7 10	ineq12d	$⊢ B = \emptyset \to rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ⋂ B = 1_{𝑜} \cap V$
12		inv1	$⊢ 1_{𝑜} \cap V = 1_{𝑜}$
13	12	a1i	$⊢ A = \emptyset \to 1_{𝑜} \cap V = 1_{𝑜}$
14	11 13	sylan9eqr	$⊢ (A = \emptyset \land B = \emptyset) \to rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ⋂ B = 1_{𝑜}$
15	3 14	eqtr4d	$⊢ (A = \emptyset \land B = \emptyset) \to A ↑_{𝑜} B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ⋂ B$
16		oveq1	$⊢ A = \emptyset \to A ↑_{𝑜} B = \emptyset ↑_{𝑜} B$
17		oe0m1	$⊢ B \in On \to (\emptyset \in B \leftrightarrow \emptyset ↑_{𝑜} B = \emptyset)$
18	17	biimpa	$⊢ (B \in On \land \emptyset \in B) \to \emptyset ↑_{𝑜} B = \emptyset$
19	16 18	sylan9eqr	$⊢ ((B \in On \land \emptyset \in B) \land A = \emptyset) \to A ↑_{𝑜} B = \emptyset$
20	19	an32s	$⊢ ((B \in On \land A = \emptyset) \land \emptyset \in B) \to A ↑_{𝑜} B = \emptyset$
21		int0el	$⊢ \emptyset \in B \to ⋂ B = \emptyset$
22	21	ineq2d	$⊢ \emptyset \in B \to rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ⋂ B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap \emptyset$
23		in0	$⊢ rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap \emptyset = \emptyset$
24	22 23	eqtrdi	$⊢ \emptyset \in B \to rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ⋂ B = \emptyset$
25	24	adantl	$⊢ ((B \in On \land A = \emptyset) \land \emptyset \in B) \to rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ⋂ B = \emptyset$
26	20 25	eqtr4d	$⊢ ((B \in On \land A = \emptyset) \land \emptyset \in B) \to A ↑_{𝑜} B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ⋂ B$
27	15 26	oe0lem	$⊢ (B \in On \land A = \emptyset) \to A ↑_{𝑜} B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ⋂ B$
28		inteq	$⊢ A = \emptyset \to ⋂ A = ⋂ \emptyset$
29	28 9	eqtrdi	$⊢ A = \emptyset \to ⋂ A = V$
30	29	difeq2d	$⊢ A = \emptyset \to V ∖ ⋂ A = V ∖ V$
31		difid	$⊢ V ∖ V = \emptyset$
32	30 31	eqtrdi	$⊢ A = \emptyset \to V ∖ ⋂ A = \emptyset$
33	32	uneq2d	$⊢ A = \emptyset \to ⋂ B \cup (V ∖ ⋂ A) = ⋂ B \cup \emptyset$
34		uncom	$⊢ ⋂ B \cup (V ∖ ⋂ A) = (V ∖ ⋂ A) \cup ⋂ B$
35		un0	$⊢ ⋂ B \cup \emptyset = ⋂ B$
36	33 34 35	3eqtr3g	$⊢ A = \emptyset \to (V ∖ ⋂ A) \cup ⋂ B = ⋂ B$
37	36	adantl	$⊢ (B \in On \land A = \emptyset) \to (V ∖ ⋂ A) \cup ⋂ B = ⋂ B$
38	37	ineq2d	$⊢ (B \in On \land A = \emptyset) \to rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ((V ∖ ⋂ A) \cup ⋂ B) = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ⋂ B$
39	27 38	eqtr4d	$⊢ (B \in On \land A = \emptyset) \to A ↑_{𝑜} B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ((V ∖ ⋂ A) \cup ⋂ B)$
40		oevn0	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to A ↑_{𝑜} B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B)$
41		int0el	$⊢ \emptyset \in A \to ⋂ A = \emptyset$
42	41	difeq2d	$⊢ \emptyset \in A \to V ∖ ⋂ A = V ∖ \emptyset$
43		dif0	$⊢ V ∖ \emptyset = V$
44	42 43	eqtrdi	$⊢ \emptyset \in A \to V ∖ ⋂ A = V$
45	44	uneq2d	$⊢ \emptyset \in A \to ⋂ B \cup (V ∖ ⋂ A) = ⋂ B \cup V$
46		unv	$⊢ ⋂ B \cup V = V$
47	45 34 46	3eqtr3g	$⊢ \emptyset \in A \to (V ∖ ⋂ A) \cup ⋂ B = V$
48	47	adantl	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to (V ∖ ⋂ A) \cup ⋂ B = V$
49	48	ineq2d	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ((V ∖ ⋂ A) \cup ⋂ B) = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap V$
50		inv1	$⊢ rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap V = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B)$
51	49 50	eqtr2di	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ((V ∖ ⋂ A) \cup ⋂ B)$
52	40 51	eqtrd	$⊢ ((A \in On \land B \in On) \land \emptyset \in A) \to A ↑_{𝑜} B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ((V ∖ ⋂ A) \cup ⋂ B)$
53	39 52	oe0lem	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B = rec ((x \in V ⟼ x \cdot_{𝑜} A), 1_{𝑜}) (B) \cap ((V ∖ ⋂ A) \cup ⋂ B)$

Metamath Proof Explorer

Theorem oev2

Proof