cantnflem1b

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 4-Jun-2015) (Revised by AV, 2-Jul-2019)

	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)))\}$
	oemapval.f	$⊢ φ \to F \in S$
	oemapval.g	$⊢ φ \to G \in S$
	oemapvali.r	$⊢ φ \to F T G$
	oemapvali.x	$⊢ X = ⋃ \{c \in B \| F (c) \in G (c)\}$
	cantnflem1.o	$⊢ O = OrdIso (E, G supp \emptyset)$
Assertion	cantnflem1b	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to X \subseteq O (u)$

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		oemapval.f	$⊢ φ \to F \in S$
6		oemapval.g	$⊢ φ \to G \in S$
7		oemapvali.r	$⊢ φ \to F T G$
8		oemapvali.x	$⊢ X = ⋃ \{c \in B \| F (c) \in G (c)\}$
9		cantnflem1.o	$⊢ O = OrdIso (E, G supp \emptyset)$
10		simprr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O^{-1} (X) \subseteq u$
11	9	oicl	$⊢ Ord dom O$
12		ovexd	$⊢ φ \to G supp \emptyset \in V$
13	1 2 3 9 6	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (G) \land dom O \in ω)$
14	13	simpld	$⊢ φ \to E We {supp}_{\emptyset} (G)$
15	9	oiiso	$⊢ (G supp \emptyset \in V \land E We {supp}_{\emptyset} (G)) \to O {Isom}_{E, E} (dom O, G supp \emptyset)$
16	12 14 15	syl2anc	$⊢ φ \to O {Isom}_{E, E} (dom O, G supp \emptyset)$
17		isof1o	$⊢ O {Isom}_{E, E} (dom O, G supp \emptyset) \to O : dom O \underset{1-1 onto}{⟶} G supp \emptyset$
18	16 17	syl	$⊢ φ \to O : dom O \underset{1-1 onto}{⟶} G supp \emptyset$
19		f1ocnv	$⊢ O : dom O \underset{1-1 onto}{⟶} G supp \emptyset \to O^{-1} : G supp \emptyset \underset{1-1 onto}{⟶} dom O$
20		f1of	$⊢ O^{-1} : G supp \emptyset \underset{1-1 onto}{⟶} dom O \to O^{-1} : G supp \emptyset ⟶ dom O$
21	18 19 20	3syl	$⊢ φ \to O^{-1} : G supp \emptyset ⟶ dom O$
22	1 2 3 4 5 6 7 8	cantnflem1a	$⊢ φ \to X \in {supp}_{\emptyset} (G)$
23	21 22	ffvelrnd	$⊢ φ \to O^{-1} (X) \in dom O$
24		ordelon	$⊢ (Ord dom O \land O^{-1} (X) \in dom O) \to O^{-1} (X) \in On$
25	11 23 24	sylancr	$⊢ φ \to O^{-1} (X) \in On$
26	11	a1i	$⊢ φ \to Ord dom O$
27		ordelon	$⊢ (Ord dom O \land suc u \in dom O) \to suc u \in On$
28	26 27	sylan	$⊢ (φ \land suc u \in dom O) \to suc u \in On$
29		sucelon	$⊢ u \in On \leftrightarrow suc u \in On$
30	28 29	sylibr	$⊢ (φ \land suc u \in dom O) \to u \in On$
31	30	adantrr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to u \in On$
32		ontri1	$⊢ (O^{-1} (X) \in On \land u \in On) \to (O^{-1} (X) \subseteq u \leftrightarrow \neg u \in O^{-1} (X))$
33	25 31 32	syl2an2r	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (O^{-1} (X) \subseteq u \leftrightarrow \neg u \in O^{-1} (X))$
34	10 33	mpbid	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to \neg u \in O^{-1} (X)$
35	16	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O {Isom}_{E, E} (dom O, G supp \emptyset)$
36		ordtr	$⊢ Ord dom O \to Tr dom O$
37	11 36	mp1i	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to Tr dom O$
38		simprl	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to suc u \in dom O$
39		trsuc	$⊢ (Tr dom O \land suc u \in dom O) \to u \in dom O$
40	37 38 39	syl2anc	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to u \in dom O$
41	23	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O^{-1} (X) \in dom O$
42		isorel	$⊢ (O {Isom}_{E, E} (dom O, G supp \emptyset) \land (u \in dom O \land O^{-1} (X) \in dom O)) \to (u E O^{-1} (X) \leftrightarrow O (u) E O (O^{-1} (X)))$
43	35 40 41 42	syl12anc	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (u E O^{-1} (X) \leftrightarrow O (u) E O (O^{-1} (X)))$
44		fvex	$⊢ O^{-1} (X) \in V$
45	44	epeli	$⊢ u E O^{-1} (X) \leftrightarrow u \in O^{-1} (X)$
46		fvex	$⊢ O (O^{-1} (X)) \in V$
47	46	epeli	$⊢ O (u) E O (O^{-1} (X)) \leftrightarrow O (u) \in O (O^{-1} (X))$
48	43 45 47	3bitr3g	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (u \in O^{-1} (X) \leftrightarrow O (u) \in O (O^{-1} (X)))$
49		f1ocnvfv2	$⊢ (O : dom O \underset{1-1 onto}{⟶} G supp \emptyset \land X \in {supp}_{\emptyset} (G)) \to O (O^{-1} (X)) = X$
50	18 22 49	syl2anc	$⊢ φ \to O (O^{-1} (X)) = X$
51	50	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (O^{-1} (X)) = X$
52	51	eleq2d	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (O (u) \in O (O^{-1} (X)) \leftrightarrow O (u) \in X)$
53	48 52	bitrd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (u \in O^{-1} (X) \leftrightarrow O (u) \in X)$
54	34 53	mtbid	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to \neg O (u) \in X$
55	1 2 3 4 5 6 7 8	oemapvali	$⊢ φ \to (X \in B \land F (X) \in G (X) \land \forall w \in B (X \in w \to F (w) = G (w)))$
56	55	simp1d	$⊢ φ \to X \in B$
57		onelon	$⊢ (B \in On \land X \in B) \to X \in On$
58	3 56 57	syl2anc	$⊢ φ \to X \in On$
59		suppssdm	$⊢ G supp \emptyset \subseteq dom G$
60	1 2 3	cantnfs	$⊢ φ \to (G \in S \leftrightarrow (G : B ⟶ A \land {finSupp}_{\emptyset} (G)))$
61	6 60	mpbid	$⊢ φ \to (G : B ⟶ A \land {finSupp}_{\emptyset} (G))$
62	61	simpld	$⊢ φ \to G : B ⟶ A$
63	59 62	fssdm	$⊢ φ \to G supp \emptyset \subseteq B$
64	63	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to G supp \emptyset \subseteq B$
65	9	oif	$⊢ O : dom O ⟶ G supp \emptyset$
66	65	ffvelrni	$⊢ u \in dom O \to O (u) \in {supp}_{\emptyset} (G)$
67	40 66	syl	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (u) \in {supp}_{\emptyset} (G)$
68	64 67	sseldd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (u) \in B$
69		onelon	$⊢ (B \in On \land O (u) \in B) \to O (u) \in On$
70	3 68 69	syl2an2r	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (u) \in On$
71		ontri1	$⊢ (X \in On \land O (u) \in On) \to (X \subseteq O (u) \leftrightarrow \neg O (u) \in X)$
72	58 70 71	syl2an2r	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (X \subseteq O (u) \leftrightarrow \neg O (u) \in X)$
73	54 72	mpbird	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to X \subseteq O (u)$

Metamath Proof Explorer

Theorem cantnflem1b

Proof