This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝒫 𝐺 ( 𝐹 ≈ 𝑖 ∧ ( 𝑖 ∪ 𝐻 ) ∈ 𝐼 ) )