cantnffval2

Description: An alternate definition of df-cnf which relies on cantnf . (Note that although the use of S seems self-referential, one can use cantnfdm to eliminate it.) (Contributed by Mario Carneiro, 28-May-2015)

	Ref	Expression
Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
Assertion	cantnffval2	$⊢ φ \to A CNF B = {OrdIso (T, S)}^{-1}$

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	$⊢ S = dom (A CNF B)$
2		cantnfs.a	$⊢ φ \to A \in On$
3		cantnfs.b	$⊢ φ \to B \in On$
4		oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
5	1 2 3 4	cantnf	$⊢ φ \to (A CNF B) {Isom}_{T, E} (S, A ↑_{𝑜} B)$
6		isof1o	$⊢ (A CNF B) {Isom}_{T, E} (S, A ↑_{𝑜} B) \to (A CNF B) : S \underset{1-1 onto}{⟶} A ↑_{𝑜} B$
7		f1orel	$⊢ (A CNF B) : S \underset{1-1 onto}{⟶} A ↑_{𝑜} B \to Rel (A CNF B)$
8	5 6 7	3syl	$⊢ φ \to Rel (A CNF B)$
9		dfrel2	$⊢ Rel (A CNF B) \leftrightarrow {(A CNF B)}^{-1}^{-1} = A CNF B$
10	8 9	sylib	$⊢ φ \to {(A CNF B)}^{-1}^{-1} = A CNF B$
11		oecl	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B \in On$
12	2 3 11	syl2anc	$⊢ φ \to A ↑_{𝑜} B \in On$
13		eloni	$⊢ A ↑_{𝑜} B \in On \to Ord (A ↑_{𝑜} B)$
14	12 13	syl	$⊢ φ \to Ord (A ↑_{𝑜} B)$
15		isocnv	$⊢ (A CNF B) {Isom}_{T, E} (S, A ↑_{𝑜} B) \to {(A CNF B)}^{-1} {Isom}_{E, T} (A ↑_{𝑜} B, S)$
16	5 15	syl	$⊢ φ \to {(A CNF B)}^{-1} {Isom}_{E, T} (A ↑_{𝑜} B, S)$
17	1 2 3 4	oemapwe	$⊢ φ \to (T We S \land dom OrdIso (T, S) = A ↑_{𝑜} B)$
18	17	simpld	$⊢ φ \to T We S$
19		ovex	$⊢ A CNF B \in V$
20	19	dmex	$⊢ dom (A CNF B) \in V$
21	1 20	eqeltri	$⊢ S \in V$
22		exse	$⊢ S \in V \to T Se S$
23	21 22	ax-mp	$⊢ T Se S$
24		eqid	$⊢ OrdIso (T, S) = OrdIso (T, S)$
25	24	oieu	$⊢ (T We S \land T Se S) \to ((Ord (A ↑_{𝑜} B) \land {(A CNF B)}^{-1} {Isom}_{E, T} (A ↑_{𝑜} B, S)) \leftrightarrow (A ↑_{𝑜} B = dom OrdIso (T, S) \land {(A CNF B)}^{-1} = OrdIso (T, S)))$
26	18 23 25	sylancl	$⊢ φ \to ((Ord (A ↑_{𝑜} B) \land {(A CNF B)}^{-1} {Isom}_{E, T} (A ↑_{𝑜} B, S)) \leftrightarrow (A ↑_{𝑜} B = dom OrdIso (T, S) \land {(A CNF B)}^{-1} = OrdIso (T, S)))$
27	14 16 26	mpbi2and	$⊢ φ \to (A ↑_{𝑜} B = dom OrdIso (T, S) \land {(A CNF B)}^{-1} = OrdIso (T, S))$
28	27	simprd	$⊢ φ \to {(A CNF B)}^{-1} = OrdIso (T, S)$
29	28	cnveqd	$⊢ φ \to {(A CNF B)}^{-1}^{-1} = {OrdIso (T, S)}^{-1}$
30	10 29	eqtr3d	$⊢ φ \to A CNF B = {OrdIso (T, S)}^{-1}$

Metamath Proof Explorer

Theorem cantnffval2

Proof