cantnflt2

Description: An upper bound on the CNF function. (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 29-Jun-2019)

	Ref	Expression
Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	cantnflt2.f	$⊢ φ \to F \in S$
	cantnflt2.a	$⊢ φ \to \emptyset \in A$
	cantnflt2.c	$⊢ φ \to C \in On$
	cantnflt2.s	$⊢ φ \to F supp \emptyset \subseteq C$
Assertion	cantnflt2	$⊢ φ \to (A CNF B) (F) \in (A ↑_{𝑜} C)$

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		cantnflt2.f	$⊢ φ \to F \in S$
5		cantnflt2.a	$⊢ φ \to \emptyset \in A$
6		cantnflt2.c	$⊢ φ \to C \in On$
7		cantnflt2.s	$⊢ φ \to F supp \emptyset \subseteq C$
8		eqid	$⊢ OrdIso (E, F supp \emptyset) = OrdIso (E, F supp \emptyset)$
9		eqid	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, F supp \emptyset) (k)) \cdot_{𝑜} F (OrdIso (E, F supp \emptyset) (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, F supp \emptyset) (k)) \cdot_{𝑜} F (OrdIso (E, F supp \emptyset) (k))) +_{𝑜} z), \emptyset)$
10	1 2 3 8 4 9	cantnfval	$⊢ φ \to (A CNF B) (F) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, F supp \emptyset) (k)) \cdot_{𝑜} F (OrdIso (E, F supp \emptyset) (k))) +_{𝑜} z), \emptyset) (dom OrdIso (E, F supp \emptyset))$
11		ovexd	$⊢ φ \to F supp \emptyset \in V$
12	8	oion	$⊢ F supp \emptyset \in V \to dom OrdIso (E, F supp \emptyset) \in On$
13		sucidg	$⊢ dom OrdIso (E, F supp \emptyset) \in On \to dom OrdIso (E, F supp \emptyset) \in suc dom OrdIso (E, F supp \emptyset)$
14	11 12 13	3syl	$⊢ φ \to dom OrdIso (E, F supp \emptyset) \in suc dom OrdIso (E, F supp \emptyset)$
15	1 2 3 8 4	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (F) \land dom OrdIso (E, F supp \emptyset) \in ω)$
16	15	simpld	$⊢ φ \to E We {supp}_{\emptyset} (F)$
17	8	oiiso	$⊢ (F supp \emptyset \in V \land E We {supp}_{\emptyset} (F)) \to OrdIso (E, F supp \emptyset) {Isom}_{E, E} (dom OrdIso (E, F supp \emptyset), F supp \emptyset)$
18	11 16 17	syl2anc	$⊢ φ \to OrdIso (E, F supp \emptyset) {Isom}_{E, E} (dom OrdIso (E, F supp \emptyset), F supp \emptyset)$
19		isof1o	$⊢ OrdIso (E, F supp \emptyset) {Isom}_{E, E} (dom OrdIso (E, F supp \emptyset), F supp \emptyset) \to OrdIso (E, F supp \emptyset) : dom OrdIso (E, F supp \emptyset) \underset{1-1 onto}{⟶} F supp \emptyset$
20		f1ofo	$⊢ OrdIso (E, F supp \emptyset) : dom OrdIso (E, F supp \emptyset) \underset{1-1 onto}{⟶} F supp \emptyset \to OrdIso (E, F supp \emptyset) : dom OrdIso (E, F supp \emptyset) \underset{onto}{⟶} F supp \emptyset$
21		foima	$⊢ OrdIso (E, F supp \emptyset) : dom OrdIso (E, F supp \emptyset) \underset{onto}{⟶} F supp \emptyset \to OrdIso (E, F supp \emptyset) [dom OrdIso (E, F supp \emptyset)] = F supp \emptyset$
22	18 19 20 21	4syl	$⊢ φ \to OrdIso (E, F supp \emptyset) [dom OrdIso (E, F supp \emptyset)] = F supp \emptyset$
23	22 7	eqsstrd	$⊢ φ \to OrdIso (E, F supp \emptyset) [dom OrdIso (E, F supp \emptyset)] \subseteq C$
24	1 2 3 8 4 9 5 14 6 23	cantnflt	$⊢ φ \to {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, F supp \emptyset) (k)) \cdot_{𝑜} F (OrdIso (E, F supp \emptyset) (k))) +_{𝑜} z), \emptyset) (dom OrdIso (E, F supp \emptyset)) \in (A ↑_{𝑜} C)$
25	10 24	eqeltrd	$⊢ φ \to (A CNF B) (F) \in (A ↑_{𝑜} C)$

Metamath Proof Explorer

Theorem cantnflt2

Proof