frgpnabllem1

Description: Lemma for frgpnabl . (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 25-Apr-2024)

	Ref	Expression
Hypotheses	frgpnabl.g	$⊢ G = freeGrp (I)$
	frgpnabl.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
	frgpnabl.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
	frgpnabl.p	$⊢ \underset{˙}{+} = +_{G}$
	frgpnabl.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
	frgpnabl.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
	frgpnabl.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
	frgpnabl.u	$⊢ U = {var}_{FGrp} (I)$
	frgpnabl.i	$⊢ φ \to I \in V$
	frgpnabl.a	$⊢ φ \to A \in I$
	frgpnabl.b	$⊢ φ \to B \in I$
Assertion	frgpnabllem1	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in (D \cap (U (A) \underset{˙}{+} U (B)))$

Proof

Step	Hyp	Ref	Expression
1		frgpnabl.g	$⊢ G = freeGrp (I)$
2		frgpnabl.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
3		frgpnabl.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
4		frgpnabl.p	$⊢ \underset{˙}{+} = +_{G}$
5		frgpnabl.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
6		frgpnabl.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
7		frgpnabl.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
8		frgpnabl.u	$⊢ U = {var}_{FGrp} (I)$
9		frgpnabl.i	$⊢ φ \to I \in V$
10		frgpnabl.a	$⊢ φ \to A \in I$
11		frgpnabl.b	$⊢ φ \to B \in I$
12		0ex	$⊢ \emptyset \in V$
13	12	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
14		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
15	13 14	eleqtrri	$⊢ \emptyset \in 2_{𝑜}$
16		opelxpi	$⊢ (A \in I \land \emptyset \in 2_{𝑜}) \to ⟨A, \emptyset⟩ \in (I \times 2_{𝑜})$
17	10 15 16	sylancl	$⊢ φ \to ⟨A, \emptyset⟩ \in (I \times 2_{𝑜})$
18		opelxpi	$⊢ (B \in I \land \emptyset \in 2_{𝑜}) \to ⟨B, \emptyset⟩ \in (I \times 2_{𝑜})$
19	11 15 18	sylancl	$⊢ φ \to ⟨B, \emptyset⟩ \in (I \times 2_{𝑜})$
20	17 19	s2cld	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in Word (I \times 2_{𝑜})$
21		2on	$⊢ 2_{𝑜} \in On$
22		xpexg	$⊢ (I \in V \land 2_{𝑜} \in On) \to I \times 2_{𝑜} \in V$
23	9 21 22	sylancl	$⊢ φ \to I \times 2_{𝑜} \in V$
24		wrdexg	$⊢ I \times 2_{𝑜} \in V \to Word (I \times 2_{𝑜}) \in V$
25		fvi	$⊢ Word (I \times 2_{𝑜}) \in V \to I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜})$
26	23 24 25	3syl	$⊢ φ \to I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜})$
27	2 26	eqtrid	$⊢ φ \to W = Word (I \times 2_{𝑜})$
28	20 27	eleqtrrd	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in W$
29		1n0	$⊢ 1_{𝑜} \neq \emptyset$
30		2cn	$⊢ 2 \in ℂ$
31	30	addid2i	$⊢ 0 + 2 = 2$
32		s2len	$⊢ \|⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩\| = 2$
33	31 32	eqtr4i	$⊢ 0 + 2 = \|⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩\|$
34	2 3 5 6	efgtlen	$⊢ (x \in W \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x)) \to \|⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩\| = \|x\| + 2$
35	34	adantll	$⊢ ((φ \land x \in W) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x)) \to \|⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩\| = \|x\| + 2$
36	33 35	eqtrid	$⊢ ((φ \land x \in W) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x)) \to 0 + 2 = \|x\| + 2$
37	36	ex	$⊢ (φ \land x \in W) \to (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x) \to 0 + 2 = \|x\| + 2)$
38		0cnd	$⊢ (φ \land x \in W) \to 0 \in ℂ$
39		simpr	$⊢ (φ \land x \in W) \to x \in W$
40	2	efgrcl	$⊢ x \in W \to (I \in V \land W = Word (I \times 2_{𝑜}))$
41	40	simprd	$⊢ x \in W \to W = Word (I \times 2_{𝑜})$
42	41	adantl	$⊢ (φ \land x \in W) \to W = Word (I \times 2_{𝑜})$
43	39 42	eleqtrd	$⊢ (φ \land x \in W) \to x \in Word (I \times 2_{𝑜})$
44		lencl	$⊢ x \in Word (I \times 2_{𝑜}) \to \|x\| \in ℕ_{0}$
45	43 44	syl	$⊢ (φ \land x \in W) \to \|x\| \in ℕ_{0}$
46	45	nn0cnd	$⊢ (φ \land x \in W) \to \|x\| \in ℂ$
47		2cnd	$⊢ (φ \land x \in W) \to 2 \in ℂ$
48	38 46 47	addcan2d	$⊢ (φ \land x \in W) \to (0 + 2 = \|x\| + 2 \leftrightarrow 0 = \|x\|)$
49	37 48	sylibd	$⊢ (φ \land x \in W) \to (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x) \to 0 = \|x\|)$
50	2 3 5 6	efgtf	$⊢ \emptyset \in W \to (T (\emptyset) = (a \in (0 \dots \|\emptyset\|), b \in (I \times 2_{𝑜}) ⟼ \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \land T (\emptyset) : (0 \dots \|\emptyset\|) \times (I \times 2_{𝑜}) ⟶ W)$
51	50	adantl	$⊢ (φ \land \emptyset \in W) \to (T (\emptyset) = (a \in (0 \dots \|\emptyset\|), b \in (I \times 2_{𝑜}) ⟼ \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \land T (\emptyset) : (0 \dots \|\emptyset\|) \times (I \times 2_{𝑜}) ⟶ W)$
52	51	simpld	$⊢ (φ \land \emptyset \in W) \to T (\emptyset) = (a \in (0 \dots \|\emptyset\|), b \in (I \times 2_{𝑜}) ⟼ \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
53	52	rneqd	$⊢ (φ \land \emptyset \in W) \to ran T (\emptyset) = ran (a \in (0 \dots \|\emptyset\|), b \in (I \times 2_{𝑜}) ⟼ \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
54	53	eleq2d	$⊢ (φ \land \emptyset \in W) \to (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (\emptyset) \leftrightarrow ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran (a \in (0 \dots \|\emptyset\|), b \in (I \times 2_{𝑜}) ⟼ \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩))$
55		eqid	$⊢ (a \in (0 \dots \|\emptyset\|), b \in (I \times 2_{𝑜}) ⟼ \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) = (a \in (0 \dots \|\emptyset\|), b \in (I \times 2_{𝑜}) ⟼ \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩)$
56		ovex	$⊢ \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \in V$
57	55 56	elrnmpo	$⊢ ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran (a \in (0 \dots \|\emptyset\|), b \in (I \times 2_{𝑜}) ⟼ \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \leftrightarrow \exists a \in (0 \dots \|\emptyset\|) \exists b \in (I \times 2_{𝑜}) ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩$
58		wrd0	$⊢ \emptyset \in Word (I \times 2_{𝑜})$
59	58	a1i	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to \emptyset \in Word (I \times 2_{𝑜})$
60		simprr	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to b \in (I \times 2_{𝑜})$
61	5	efgmf	$⊢ M : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
62	61	ffvelrni	$⊢ b \in (I \times 2_{𝑜}) \to M (b) \in (I \times 2_{𝑜})$
63	60 62	syl	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to M (b) \in (I \times 2_{𝑜})$
64	60 63	s2cld	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to ⟨“ b M (b) ”⟩ \in Word (I \times 2_{𝑜})$
65		ccatidid	$⊢ \emptyset ++ \emptyset = \emptyset$
66	65	oveq1i	$⊢ (\emptyset ++ \emptyset) ++ \emptyset = \emptyset ++ \emptyset$
67	66 65	eqtr2i	$⊢ \emptyset = (\emptyset ++ \emptyset) ++ \emptyset$
68	67	a1i	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to \emptyset = (\emptyset ++ \emptyset) ++ \emptyset$
69		simprl	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to a \in (0 \dots \|\emptyset\|)$
70		hash0	$⊢ \|\emptyset\| = 0$
71	70	oveq2i	$⊢ (0 \dots \|\emptyset\|) = (0 \dots 0)$
72	69 71	eleqtrdi	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to a \in (0 \dots 0)$
73		elfz1eq	$⊢ a \in (0 \dots 0) \to a = 0$
74	72 73	syl	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to a = 0$
75	74 70	eqtr4di	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to a = \|\emptyset\|$
76	70	oveq2i	$⊢ a + \|\emptyset\| = a + 0$
77		0cn	$⊢ 0 \in ℂ$
78	74 77	eqeltrdi	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to a \in ℂ$
79	78	addid1d	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to a + 0 = a$
80	76 79	eqtr2id	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to a = a + \|\emptyset\|$
81	59 59 59 64 68 75 80	splval2	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ = (\emptyset ++ ⟨“ b M (b) ”⟩) ++ \emptyset$
82		ccatlid	$⊢ ⟨“ b M (b) ”⟩ \in Word (I \times 2_{𝑜}) \to \emptyset ++ ⟨“ b M (b) ”⟩ = ⟨“ b M (b) ”⟩$
83	82	oveq1d	$⊢ ⟨“ b M (b) ”⟩ \in Word (I \times 2_{𝑜}) \to (\emptyset ++ ⟨“ b M (b) ”⟩) ++ \emptyset = ⟨“ b M (b) ”⟩ ++ \emptyset$
84		ccatrid	$⊢ ⟨“ b M (b) ”⟩ \in Word (I \times 2_{𝑜}) \to ⟨“ b M (b) ”⟩ ++ \emptyset = ⟨“ b M (b) ”⟩$
85	83 84	eqtrd	$⊢ ⟨“ b M (b) ”⟩ \in Word (I \times 2_{𝑜}) \to (\emptyset ++ ⟨“ b M (b) ”⟩) ++ \emptyset = ⟨“ b M (b) ”⟩$
86	64 85	syl	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to (\emptyset ++ ⟨“ b M (b) ”⟩) ++ \emptyset = ⟨“ b M (b) ”⟩$
87	81 86	eqtrd	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ = ⟨“ b M (b) ”⟩$
88	87	eqeq2d	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \leftrightarrow ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩)$
89	10	ad3antrrr	$⊢ (((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩) \to A \in I$
90		1on	$⊢ 1_{𝑜} \in On$
91	90	a1i	$⊢ (((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩) \to 1_{𝑜} \in On$
92		simpr	$⊢ (((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩) \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩$
93	92	fveq1d	$⊢ (((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩) \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ (1) = ⟨“ b M (b) ”⟩ (1)$
94		opex	$⊢ ⟨B, \emptyset⟩ \in V$
95		s2fv1	$⊢ ⟨B, \emptyset⟩ \in V \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ (1) = ⟨B, \emptyset⟩$
96	94 95	ax-mp	$⊢ ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ (1) = ⟨B, \emptyset⟩$
97		fvex	$⊢ M (b) \in V$
98		s2fv1	$⊢ M (b) \in V \to ⟨“ b M (b) ”⟩ (1) = M (b)$
99	97 98	ax-mp	$⊢ ⟨“ b M (b) ”⟩ (1) = M (b)$
100	93 96 99	3eqtr3g	$⊢ (((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩) \to ⟨B, \emptyset⟩ = M (b)$
101	92	fveq1d	$⊢ (((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩) \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ (0) = ⟨“ b M (b) ”⟩ (0)$
102		opex	$⊢ ⟨A, \emptyset⟩ \in V$
103		s2fv0	$⊢ ⟨A, \emptyset⟩ \in V \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ (0) = ⟨A, \emptyset⟩$
104	102 103	ax-mp	$⊢ ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ (0) = ⟨A, \emptyset⟩$
105		s2fv0	$⊢ b \in V \to ⟨“ b M (b) ”⟩ (0) = b$
106	105	elv	$⊢ ⟨“ b M (b) ”⟩ (0) = b$
107	101 104 106	3eqtr3g	$⊢ (((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩) \to ⟨A, \emptyset⟩ = b$
108	107	fveq2d	$⊢ (((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩) \to M (⟨A, \emptyset⟩) = M (b)$
109	5	efgmval	$⊢ (A \in I \land \emptyset \in 2_{𝑜}) \to A M \emptyset = ⟨A, 1_{𝑜} ∖ \emptyset⟩$
110	89 15 109	sylancl	$⊢ (((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩) \to A M \emptyset = ⟨A, 1_{𝑜} ∖ \emptyset⟩$
111		df-ov	$⊢ A M \emptyset = M (⟨A, \emptyset⟩)$
112		dif0	$⊢ 1_{𝑜} ∖ \emptyset = 1_{𝑜}$
113	112	opeq2i	$⊢ ⟨A, 1_{𝑜} ∖ \emptyset⟩ = ⟨A, 1_{𝑜}⟩$
114	110 111 113	3eqtr3g	$⊢ (((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩) \to M (⟨A, \emptyset⟩) = ⟨A, 1_{𝑜}⟩$
115	100 108 114	3eqtr2rd	$⊢ (((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩) \to ⟨A, 1_{𝑜}⟩ = ⟨B, \emptyset⟩$
116		opthg	$⊢ (A \in I \land 1_{𝑜} \in On) \to (⟨A, 1_{𝑜}⟩ = ⟨B, \emptyset⟩ \leftrightarrow (A = B \land 1_{𝑜} = \emptyset))$
117	116	simplbda	$⊢ ((A \in I \land 1_{𝑜} \in On) \land ⟨A, 1_{𝑜}⟩ = ⟨B, \emptyset⟩) \to 1_{𝑜} = \emptyset$
118	89 91 115 117	syl21anc	$⊢ (((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩) \to 1_{𝑜} = \emptyset$
119	118	ex	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ b M (b) ”⟩ \to 1_{𝑜} = \emptyset)$
120	88 119	sylbid	$⊢ ((φ \land \emptyset \in W) \land (a \in (0 \dots \|\emptyset\|) \land b \in (I \times 2_{𝑜}))) \to (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \to 1_{𝑜} = \emptyset)$
121	120	rexlimdvva	$⊢ (φ \land \emptyset \in W) \to (\exists a \in (0 \dots \|\emptyset\|) \exists b \in (I \times 2_{𝑜}) ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩ \to 1_{𝑜} = \emptyset)$
122	57 121	syl5bi	$⊢ (φ \land \emptyset \in W) \to (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran (a \in (0 \dots \|\emptyset\|), b \in (I \times 2_{𝑜}) ⟼ \emptyset splice ⟨a, a, ⟨“ b M (b) ”⟩⟩) \to 1_{𝑜} = \emptyset)$
123	54 122	sylbid	$⊢ (φ \land \emptyset \in W) \to (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (\emptyset) \to 1_{𝑜} = \emptyset)$
124	123	expimpd	$⊢ φ \to ((\emptyset \in W \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (\emptyset)) \to 1_{𝑜} = \emptyset)$
125		hasheq0	$⊢ x \in V \to (\|x\| = 0 \leftrightarrow x = \emptyset)$
126	125	elv	$⊢ \|x\| = 0 \leftrightarrow x = \emptyset$
127		eleq1	$⊢ x = \emptyset \to (x \in W \leftrightarrow \emptyset \in W)$
128		fveq2	$⊢ x = \emptyset \to T (x) = T (\emptyset)$
129	128	rneqd	$⊢ x = \emptyset \to ran T (x) = ran T (\emptyset)$
130	129	eleq2d	$⊢ x = \emptyset \to (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x) \leftrightarrow ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (\emptyset))$
131	127 130	anbi12d	$⊢ x = \emptyset \to ((x \in W \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x)) \leftrightarrow (\emptyset \in W \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (\emptyset)))$
132	126 131	sylbi	$⊢ \|x\| = 0 \to ((x \in W \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x)) \leftrightarrow (\emptyset \in W \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (\emptyset)))$
133	132	eqcoms	$⊢ 0 = \|x\| \to ((x \in W \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x)) \leftrightarrow (\emptyset \in W \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (\emptyset)))$
134	133	imbi1d	$⊢ 0 = \|x\| \to (((x \in W \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x)) \to 1_{𝑜} = \emptyset) \leftrightarrow ((\emptyset \in W \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (\emptyset)) \to 1_{𝑜} = \emptyset))$
135	124 134	syl5ibrcom	$⊢ φ \to (0 = \|x\| \to ((x \in W \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x)) \to 1_{𝑜} = \emptyset))$
136	135	com23	$⊢ φ \to ((x \in W \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x)) \to (0 = \|x\| \to 1_{𝑜} = \emptyset))$
137	136	expdimp	$⊢ (φ \land x \in W) \to (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x) \to (0 = \|x\| \to 1_{𝑜} = \emptyset))$
138	49 137	mpdd	$⊢ (φ \land x \in W) \to (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x) \to 1_{𝑜} = \emptyset)$
139	138	necon3ad	$⊢ (φ \land x \in W) \to (1_{𝑜} \neq \emptyset \to \neg ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x))$
140	29 139	mpi	$⊢ (φ \land x \in W) \to \neg ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x)$
141	140	nrexdv	$⊢ φ \to \neg \exists x \in W ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x)$
142		eliun	$⊢ ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ⋃_{x \in W} ran T (x) \leftrightarrow \exists x \in W ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ran T (x)$
143	141 142	sylnibr	$⊢ φ \to \neg ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in ⋃_{x \in W} ran T (x)$
144	28 143	eldifd	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in (W ∖ ⋃_{x \in W} ran T (x))$
145	144 7	eleqtrrdi	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in D$
146		df-s2	$⊢ ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ ⟨A, \emptyset⟩ ”⟩ ++ ⟨“ ⟨B, \emptyset⟩ ”⟩$
147	2 3	efger	$⊢ \underset{˙}{\sim} Er W$
148	147	a1i	$⊢ φ \to \underset{˙}{\sim} Er W$
149	148 28	erref	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \underset{˙}{\sim} ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩$
150	146 149	eqbrtrrid	$⊢ φ \to (⟨“ ⟨A, \emptyset⟩ ”⟩ ++ ⟨“ ⟨B, \emptyset⟩ ”⟩) \underset{˙}{\sim} ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩$
151	146	ovexi	$⊢ ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in V$
152		ovex	$⊢ ⟨“ ⟨A, \emptyset⟩ ”⟩ ++ ⟨“ ⟨B, \emptyset⟩ ”⟩ \in V$
153	151 152	elec	$⊢ ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in [(⟨“ ⟨A, \emptyset⟩ ”⟩ ++ ⟨“ ⟨B, \emptyset⟩ ”⟩)] \underset{˙}{\sim} \leftrightarrow (⟨“ ⟨A, \emptyset⟩ ”⟩ ++ ⟨“ ⟨B, \emptyset⟩ ”⟩) \underset{˙}{\sim} ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩$
154	150 153	sylibr	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in [(⟨“ ⟨A, \emptyset⟩ ”⟩ ++ ⟨“ ⟨B, \emptyset⟩ ”⟩)] \underset{˙}{\sim}$
155	3 8	vrgpval	$⊢ (I \in V \land A \in I) \to U (A) = [⟨“ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
156	9 10 155	syl2anc	$⊢ φ \to U (A) = [⟨“ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
157	3 8	vrgpval	$⊢ (I \in V \land B \in I) \to U (B) = [⟨“ ⟨B, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
158	9 11 157	syl2anc	$⊢ φ \to U (B) = [⟨“ ⟨B, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
159	156 158	oveq12d	$⊢ φ \to U (A) \underset{˙}{+} U (B) = [⟨“ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨“ ⟨B, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
160	17	s1cld	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ”⟩ \in Word (I \times 2_{𝑜})$
161	160 27	eleqtrrd	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ”⟩ \in W$
162	19	s1cld	$⊢ φ \to ⟨“ ⟨B, \emptyset⟩ ”⟩ \in Word (I \times 2_{𝑜})$
163	162 27	eleqtrrd	$⊢ φ \to ⟨“ ⟨B, \emptyset⟩ ”⟩ \in W$
164	2 1 3 4	frgpadd	$⊢ (⟨“ ⟨A, \emptyset⟩ ”⟩ \in W \land ⟨“ ⟨B, \emptyset⟩ ”⟩ \in W) \to [⟨“ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨“ ⟨B, \emptyset⟩ ”⟩] \underset{˙}{\sim} = [(⟨“ ⟨A, \emptyset⟩ ”⟩ ++ ⟨“ ⟨B, \emptyset⟩ ”⟩)] \underset{˙}{\sim}$
165	161 163 164	syl2anc	$⊢ φ \to [⟨“ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim} \underset{˙}{+} [⟨“ ⟨B, \emptyset⟩ ”⟩] \underset{˙}{\sim} = [(⟨“ ⟨A, \emptyset⟩ ”⟩ ++ ⟨“ ⟨B, \emptyset⟩ ”⟩)] \underset{˙}{\sim}$
166	159 165	eqtrd	$⊢ φ \to U (A) \underset{˙}{+} U (B) = [(⟨“ ⟨A, \emptyset⟩ ”⟩ ++ ⟨“ ⟨B, \emptyset⟩ ”⟩)] \underset{˙}{\sim}$
167	154 166	eleqtrrd	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in (U (A) \underset{˙}{+} U (B))$
168	145 167	elind	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in (D \cap (U (A) \underset{˙}{+} U (B)))$

Metamath Proof Explorer

Theorem frgpnabllem1

Proof