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		difexg	$⊢ X \in J \to X ∖ H \in V$
43	1 42	syl	$⊢ φ \to X ∖ H \in V$
44	43 2	sselpwd	$⊢ φ \to F \in 𝒫 (X ∖ H)$
45	44	adantr	$⊢ (φ \land h = H) \to F \in 𝒫 (X ∖ H)$
46		simpr	$⊢ (φ \land h = H) \to h = H$
47	46	difeq2d	$⊢ (φ \land h = H) \to X ∖ h = X ∖ H$
48	47	pweqd	$⊢ (φ \land h = H) \to 𝒫 (X ∖ h) = 𝒫 (X ∖ H)$
49	45 48	eleqtrrd	$⊢ (φ \land h = H) \to F \in 𝒫 (X ∖ h)$
50	43 3	sselpwd	$⊢ φ \to G \in 𝒫 (X ∖ H)$
51	50	ad2antrr	$⊢ ((φ \land h = H) \land f = F) \to G \in 𝒫 (X ∖ H)$
52	48	adantr	$⊢ ((φ \land h = H) \land f = F) \to 𝒫 (X ∖ h) = 𝒫 (X ∖ H)$
53	51 52	eleqtrrd	$⊢ ((φ \land h = H) \land f = F) \to G \in 𝒫 (X ∖ h)$
54		simplr	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to f = F$
55	54	breq1d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (f \approx K \leftrightarrow F \approx K)$
56		simpr	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to g = G$
57	56	breq1d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (g \approx K \leftrightarrow G \approx K)$
58	55 57	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))$
59		simpllr	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to h = H$
60	56 59	uneq12d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to g \cup h = G \cup H$
61	60	fveq2d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to N (g \cup h) = N (G \cup H)$
62	54 61	sseq12d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (f \subseteq N (g \cup h) \leftrightarrow F \subseteq N (G \cup H))$
63	54 59	uneq12d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to f \cup h = F \cup H$
64	63	eleq1d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (f \cup h \in I \leftrightarrow F \cup H \in I)$
65	58 62 64	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))$
66	56	pweqd	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to 𝒫 g = 𝒫 G$
67	54	breq1d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (f \approx j \leftrightarrow F \approx j)$
68	59	uneq2d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to j \cup h = j \cup H$
69	68	eleq1d	$⊢ (((φ \land h = H) \land f = F) \land g = G) \to (j \cup h \in I \leftrightarrow j \cup H \in I)$
70	67 69	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))$
71	66 70	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))$
72	65 71	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)))$
73	53 72	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)))$
74	49 73	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)))$
75	41 74	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)))$
76	38 75	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))$
77	6 4 5 76	mp3and	$⊢ φ \to \exists j \in 𝒫 G (F \approx j \land j \cup H \in I)$

Metamath Proof Explorer

Theorem mreexexlemd

Proof