mreexexlemd

Description: This lemma is used to generate substitution instances of the induction hypothesis in mreexexd . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mreexexlemd.1	$⊢ φ \to X \in J$
	mreexexlemd.2	$⊢ φ \to F \subseteq X ∖ H$
	mreexexlemd.3	$⊢ φ \to G \subseteq X ∖ H$
	mreexexlemd.4	$⊢ φ \to F \subseteq N (G \cup H)$
	mreexexlemd.5	$⊢ φ \to F \cup H \in I$
	mreexexlemd.6	$⊢ φ \to (F \approx K \lor G \approx K)$
	mreexexlemd.7	$⊢ φ \to \forall t \forall u \in 𝒫 (X ∖ t) \forall v \in 𝒫 (X ∖ t) (((u \approx K \lor v \approx K) \land u \subseteq N (v \cup t) \land u \cup t \in I) \to \exists i \in 𝒫 v (u \approx i \land i \cup t \in I))$
Assertion	mreexexlemd	$⊢ φ \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$

Proof

Step	Hyp	Ref	Expression
1		mreexexlemd.1	$⊢ φ \to X \in J$
2		mreexexlemd.2	$⊢ φ \to F \subseteq X ∖ H$
3		mreexexlemd.3	$⊢ φ \to G \subseteq X ∖ H$
4		mreexexlemd.4	$⊢ φ \to F \subseteq N (G \cup H)$
5		mreexexlemd.5	$⊢ φ \to F \cup H \in I$
6		mreexexlemd.6	$⊢ φ \to (F \approx K \lor G \approx K)$
7		mreexexlemd.7	$⊢ φ \to \forall t \forall u \in 𝒫 (X ∖ t) \forall v \in 𝒫 (X ∖ t) (((u \approx K \lor v \approx K) \land u \subseteq N (v \cup t) \land u \cup t \in I) \to \exists i \in 𝒫 v (u \approx i \land i \cup t \in I))$
8		simplr	$⊢ ((t = h \land u = f) \land v = g) \to u = f$
9	8	breq1d	$⊢ ((t = h \land u = f) \land v = g) \to (u \approx K \leftrightarrow f \approx K)$
10		simpr	$⊢ ((t = h \land u = f) \land v = g) \to v = g$
11	10	breq1d	$⊢ ((t = h \land u = f) \land v = g) \to (v \approx K \leftrightarrow g \approx K)$
12	9 11	orbi12d	$⊢ ((t = h \land u = f) \land v = g) \to ((u \approx K \lor v \approx K) \leftrightarrow (f \approx K \lor g \approx K))$
13		simpll	$⊢ ((t = h \land u = f) \land v = g) \to t = h$
14	10 13	uneq12d	$⊢ ((t = h \land u = f) \land v = g) \to v \cup t = g \cup h$
15	14	fveq2d	$⊢ ((t = h \land u = f) \land v = g) \to N (v \cup t) = N (g \cup h)$
16	8 15	sseq12d	$⊢ ((t = h \land u = f) \land v = g) \to (u \subseteq N (v \cup t) \leftrightarrow f \subseteq N (g \cup h))$
17	8 13	uneq12d	$⊢ ((t = h \land u = f) \land v = g) \to u \cup t = f \cup h$
18	17	eleq1d	$⊢ ((t = h \land u = f) \land v = g) \to (u \cup t \in I \leftrightarrow f \cup h \in I)$
19	12 16 18	3anbi123d	$⊢ ((t = h \land u = f) \land v = g) \to (((u \approx K \lor v \approx K) \land u \subseteq N (v \cup t) \land u \cup t \in I) \leftrightarrow ((f \approx K \lor g \approx K) \land f \subseteq N (g \cup h) \land f \cup h \in I))$
20		simpllr	$⊢ (((t = h \land u = f) \land v = g) \land i = j) \to u = f$
21		simpr	$⊢ (((t = h \land u = f) \land v = g) \land i = j) \to i = j$
22	20 21	breq12d	$⊢ (((t = h \land u = f) \land v = g) \land i = j) \to (u \approx i \leftrightarrow f \approx j)$
23		simplll	$⊢ (((t = h \land u = f) \land v = g) \land i = j) \to t = h$
24	21 23	uneq12d	$⊢ (((t = h \land u = f) \land v = g) \land i = j) \to i \cup t = j \cup h$
25	24	eleq1d	$⊢ (((t = h \land u = f) \land v = g) \land i = j) \to (i \cup t \in I \leftrightarrow j \cup h \in I)$
26	22 25	anbi12d	$⊢ (((t = h \land u = f) \land v = g) \land i = j) \to ((u \approx i \land i \cup t \in I) \leftrightarrow (f \approx j \land j \cup h \in I))$
27		simplr	$⊢ (((t = h \land u = f) \land v = g) \land i = j) \to v = g$
28	27	pweqd	$⊢ (((t = h \land u = f) \land v = g) \land i = j) \to 𝒫 v = 𝒫 g$
29	26 28	cbvrexdva2	$⊢ ((t = h \land u = f) \land v = g) \to (\exists i \in 𝒫 v (u \approx i \land i \cup t \in I) \leftrightarrow \exists j \in 𝒫 g (f \approx j \land j \cup h \in I))$
30	19 29	imbi12d	$⊢ ((t = h \land u = f) \land v = g) \to ((((u \approx K \lor v \approx K) \land u \subseteq N (v \cup t) \land u \cup t \in I) \to \exists i \in 𝒫 v (u \approx i \land i \cup t \in I)) \leftrightarrow (((f \approx K \lor g \approx K) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists j \in 𝒫 g (f \approx j \land j \cup h \in I)))$
31		simpl	$⊢ (t = h \land u = f) \to t = h$
32	31	difeq2d	$⊢ (t = h \land u = f) \to X ∖ t = X ∖ h$
33	32	pweqd	$⊢ (t = h \land u = f) \to 𝒫 (X ∖ t) = 𝒫 (X ∖ h)$
34	33	adantr	$⊢ ((t = h \land u = f) \land v = g) \to 𝒫 (X ∖ t) = 𝒫 (X ∖ h)$
35	30 34	cbvraldva2	$⊢ (t = h \land u = f) \to (\forall v \in 𝒫 (X ∖ t) (((u \approx K \lor v \approx K) \land u \subseteq N (v \cup t) \land u \cup t \in I) \to \exists i \in 𝒫 v (u \approx i \land i \cup t \in I)) \leftrightarrow \forall g \in 𝒫 (X ∖ h) (((f \approx K \lor g \approx K) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists j \in 𝒫 g (f \approx j \land j \cup h \in I)))$
36	35 33	cbvraldva2	$⊢ t = h \to (\forall u \in 𝒫 (X ∖ t) \forall v \in 𝒫 (X ∖ t) (((u \approx K \lor v \approx K) \land u \subseteq N (v \cup t) \land u \cup t \in I) \to \exists i \in 𝒫 v (u \approx i \land i \cup t \in I)) \leftrightarrow \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx K \lor g \approx K) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists j \in 𝒫 g (f \approx j \land j \cup h \in I)))$
37	36	cbvalvw	$⊢ \forall t \forall u \in 𝒫 (X ∖ t) \forall v \in 𝒫 (X ∖ t) (((u \approx K \lor v \approx K) \land u \subseteq N (v \cup t) \land u \cup t \in I) \to \exists i \in 𝒫 v (u \approx i \land i \cup t \in I)) \leftrightarrow \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx K \lor g \approx K) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists j \in 𝒫 g (f \approx j \land j \cup h \in I))$
38	7 37	sylib	$⊢ φ \to \forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx K \lor g \approx K) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists j \in 𝒫 g (f \approx j \land j \cup h \in I))$
39		ssun2	$⊢ H \subseteq F \cup H$
40	39	a1i	$⊢ φ \to H \subseteq F \cup H$
41	5 40	ssexd	$⊢ φ \to H \in V$
42	1	difexd	$⊢ φ \to X ∖ H \in V$
43	42 2	sselpwd	$⊢ φ \to F \in 𝒫 (X ∖ H)$
44	43	adantr	$⊢ (φ \land h = H) \to F \in 𝒫 (X ∖ H)$
45		simpr	$⊢ (φ \land h = H) \to h = H$
46	45	difeq2d	$⊢ (φ \land h = H) \to X ∖ h = X ∖ H$
47	46	pweqd	$⊢ (φ \land h = H) \to 𝒫 (X ∖ h) = 𝒫 (X ∖ H)$
48	44 47	eleqtrrd	$⊢ (φ \land h = H) \to F \in 𝒫 (X ∖ h)$
49	42 3	sselpwd	$⊢ φ \to G \in 𝒫 (X ∖ H)$
50	49	ad2antrr	$⊢ ((φ \land h = H) \land f = F) \to G \in 𝒫 (X ∖ H)$
51	47	adantr	$⊢ ((φ \land h = H) \land f = F) \to 𝒫 (X ∖ h) = 𝒫 (X ∖ H)$
52	50 51	eleqtrrd	$⊢ ((φ \land h = H) \land f = F) \to G \in 𝒫 (X ∖ h)$
53		simplr	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to f = F$
54	53	breq1d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (f \approx K \leftrightarrow F \approx K)$
55		simpr	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to g = G$
56	55	breq1d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (g \approx K \leftrightarrow G \approx K)$
57	54 56	orbi12d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to ((f \approx K \lor g \approx K) \leftrightarrow (F \approx K \lor G \approx K))$
58		simpllr	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to h = H$
59	55 58	uneq12d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to g \cup h = G \cup H$
60	59	fveq2d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to N (g \cup h) = N (G \cup H)$
61	53 60	sseq12d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (f \subseteq N (g \cup h) \leftrightarrow F \subseteq N (G \cup H))$
62	53 58	uneq12d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to f \cup h = F \cup H$
63	62	eleq1d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (f \cup h \in I \leftrightarrow F \cup H \in I)$
64	57 61 63	3anbi123d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (((f \approx K \lor g \approx K) \land f \subseteq N (g \cup h) \land f \cup h \in I) \leftrightarrow ((F \approx K \lor G \approx K) \land F \subseteq N (G \cup H) \land F \cup H \in I))$
65	55	pweqd	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to 𝒫 g = 𝒫 G$
66	53	breq1d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (f \approx j \leftrightarrow F \approx j)$
67	58	uneq2d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to j \cup h = j \cup H$
68	67	eleq1d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (j \cup h \in I \leftrightarrow j \cup H \in I)$
69	66 68	anbi12d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to ((f \approx j \land j \cup h \in I) \leftrightarrow (F \approx j \land j \cup H \in I))$
70	65 69	rexeqbidv	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (\exists j \in 𝒫 g (f \approx j \land j \cup h \in I) \leftrightarrow \exists j \in 𝒫 G (F \approx j \land j \cup H \in I))$
71	64 70	imbi12d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to ((((f \approx K \lor g \approx K) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists j \in 𝒫 g (f \approx j \land j \cup h \in I)) \leftrightarrow (((F \approx K \lor G \approx K) \land F \subseteq N (G \cup H) \land F \cup H \in I) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)))$
72	52 71	rspcdv	$⊢ ((φ \land h = H) \land f = F) \to (\forall g \in 𝒫 (X ∖ h) (((f \approx K \lor g \approx K) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists j \in 𝒫 g (f \approx j \land j \cup h \in I)) \to (((F \approx K \lor G \approx K) \land F \subseteq N (G \cup H) \land F \cup H \in I) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)))$
73	48 72	rspcimdv	$⊢ (φ \land h = H) \to (\forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx K \lor g \approx K) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists j \in 𝒫 g (f \approx j \land j \cup h \in I)) \to (((F \approx K \lor G \approx K) \land F \subseteq N (G \cup H) \land F \cup H \in I) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)))$
74	41 73	spcimdv	$⊢ φ \to (\forall h \forall f \in 𝒫 (X ∖ h) \forall g \in 𝒫 (X ∖ h) (((f \approx K \lor g \approx K) \land f \subseteq N (g \cup h) \land f \cup h \in I) \to \exists j \in 𝒫 g (f \approx j \land j \cup h \in I)) \to (((F \approx K \lor G \approx K) \land F \subseteq N (G \cup H) \land F \cup H \in I) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)))$
75	38 74	mpd	$⊢ φ \to (((F \approx K \lor G \approx K) \land F \subseteq N (G \cup H) \land F \cup H \in I) \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I))$
76	6 4 5 75	mp3and	$⊢ φ \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$

Metamath Proof Explorer

Theorem mreexexlemd

Proof