Theorem mreexexlem3d

Description: Base case of the induction in mreexexd . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mreexexlem2d.1	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
	mreexexlem2d.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	mreexexlem2d.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
	mreexexlem2d.4	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
	mreexexlem2d.5	⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑋 ∖ 𝐻 ) )
	mreexexlem2d.6	⊢ ( 𝜑 → 𝐺 ⊆ ( 𝑋 ∖ 𝐻 ) )
	mreexexlem2d.7	⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
	mreexexlem2d.8	⊢ ( 𝜑 → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
	mreexexlem3d.9	⊢ ( 𝜑 → ( 𝐹 = ∅ ∨ 𝐺 = ∅ ) )
Assertion	mreexexlem3d	⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝐻 ) ∈ 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		mreexexlem2d.1	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
2		mreexexlem2d.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3		mreexexlem2d.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4		mreexexlem2d.4	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
5		mreexexlem2d.5	⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑋 ∖ 𝐻 ) )
6		mreexexlem2d.6	⊢ ( 𝜑 → 𝐺 ⊆ ( 𝑋 ∖ 𝐻 ) )
7		mreexexlem2d.7	⊢ ( 𝜑 → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
8		mreexexlem2d.8	⊢ ( 𝜑 → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
9		mreexexlem3d.9	⊢ ( 𝜑 → ( 𝐹 = ∅ ∨ 𝐺 = ∅ ) )
10		simpr	⊢ ( ( 𝜑 ∧ 𝐹 = ∅ ) → 𝐹 = ∅ )
11	1	adantr	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
12	7	adantr	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
13		simpr	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐺 = ∅ )
14	13	uneq1d	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → ( 𝐺 ∪ 𝐻 ) = ( ∅ ∪ 𝐻 ) )
15		uncom	⊢ ( 𝐻 ∪ ∅ ) = ( ∅ ∪ 𝐻 )
16		un0	⊢ ( 𝐻 ∪ ∅ ) = 𝐻
17	15 16	eqtr3i	⊢ ( ∅ ∪ 𝐻 ) = 𝐻
18	14 17	eqtrdi	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → ( 𝐺 ∪ 𝐻 ) = 𝐻 )
19	18	fveq2d	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) = ( 𝑁 ‘ 𝐻 ) )
20	12 19	sseqtrd	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐹 ⊆ ( 𝑁 ‘ 𝐻 ) )
21	8	adantr	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
22	3 11 21	mrissd	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → ( 𝐹 ∪ 𝐻 ) ⊆ 𝑋 )
23	22	unssbd	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐻 ⊆ 𝑋 )
24	11 2 23	mrcssidd	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐻 ⊆ ( 𝑁 ‘ 𝐻 ) )
25	20 24	unssd	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → ( 𝐹 ∪ 𝐻 ) ⊆ ( 𝑁 ‘ 𝐻 ) )
26		ssun2	⊢ 𝐻 ⊆ ( 𝐹 ∪ 𝐻 )
27	26	a1i	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐻 ⊆ ( 𝐹 ∪ 𝐻 ) )
28	11 2 3 25 27 21	mrissmrcd	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → ( 𝐹 ∪ 𝐻 ) = 𝐻 )
29		ssequn1	⊢ ( 𝐹 ⊆ 𝐻 ↔ ( 𝐹 ∪ 𝐻 ) = 𝐻 )
30	28 29	sylibr	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐹 ⊆ 𝐻 )
31	5	adantr	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐹 ⊆ ( 𝑋 ∖ 𝐻 ) )
32	30 31	ssind	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐹 ⊆ ( 𝐻 ∩ ( 𝑋 ∖ 𝐻 ) ) )
33		disjdif	⊢ ( 𝐻 ∩ ( 𝑋 ∖ 𝐻 ) ) = ∅
34	32 33	sseqtrdi	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐹 ⊆ ∅ )
35		ss0b	⊢ ( 𝐹 ⊆ ∅ ↔ 𝐹 = ∅ )
36	34 35	sylib	⊢ ( ( 𝜑 ∧ 𝐺 = ∅ ) → 𝐹 = ∅ )
37	10 36 9	mpjaodan	⊢ ( 𝜑 → 𝐹 = ∅ )
38		0elpw	⊢ ∅ ∈ 𝒫 𝐺
39	37 38	eqeltrdi	⊢ ( 𝜑 → 𝐹 ∈ 𝒫 𝐺 )
40	1	elfvexd	⊢ ( 𝜑 → 𝑋 ∈ V )
41	5	difss2d	⊢ ( 𝜑 → 𝐹 ⊆ 𝑋 )
42	40 41	ssexd	⊢ ( 𝜑 → 𝐹 ∈ V )
43		enrefg	⊢ ( 𝐹 ∈ V → 𝐹 ≈ 𝐹 )
44	42 43	syl	⊢ ( 𝜑 → 𝐹 ≈ 𝐹 )
45		breq2	⊢ ( 𝑖 = 𝐹 → ( 𝐹 ≈ 𝑖 ↔ 𝐹 ≈ 𝐹 ) )
46		uneq1	⊢ ( 𝑖 = 𝐹 → ( 𝑖 ∪ 𝐻 ) = ( 𝐹 ∪ 𝐻 ) )
47	46	eleq1d	⊢ ( 𝑖 = 𝐹 → ( ( 𝑖 ∪ 𝐻 ) ∈ 𝐼 ↔ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) )
48	45 47	anbi12d	⊢ ( 𝑖 = 𝐹 → ( ( 𝐹 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝐻 ) ∈ 𝐼 ) ↔ ( 𝐹 ≈ 𝐹 ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) ) )
49	48	rspcev	⊢ ( ( 𝐹 ∈ 𝒫 𝐺 ∧ ( 𝐹 ≈ 𝐹 ∧ ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 ) ) → ∃ 𝑖 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝐻 ) ∈ 𝐼 ) )
50	39 44 8 49	syl12anc	⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝐻 ) ∈ 𝐼 ) )