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

Metamath Proof Explorer

Theorem mreexexlem2d

Description: Used in mreexexlem4d to prove the induction step in mreexexd . See the proof of Proposition 4.2.1 in FaureFrolicher p. 86 to 87. (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 ⊢ ( 𝜑 → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
mreexexlem2d.9 ⊢ ( 𝜑 → 𝑌 ∈ 𝐹 )
Assertion mreexexlem2d ( 𝜑 → ∃ 𝑔 ∈ 𝐺 ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) )

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 mreexexlem2d.9 ⊢ ( 𝜑 → 𝑌 ∈ 𝐹 )
10 7 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → 𝐹 ⊆ ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) )
11 1 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
13 ssun2 ⊢ 𝐻 ⊆ ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 )
14 difundir ⊢ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) = ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∖ { 𝑌 } ) )
15 incom ⊢ ( 𝐹 ∩ 𝐻 ) = ( 𝐻 ∩ 𝐹 )
16 ssdifin0 ⊢ ( 𝐹 ⊆ ( 𝑋 ∖ 𝐻 ) → ( 𝐹 ∩ 𝐻 ) = ∅ )
17 5 16 syl ⊢ ( 𝜑 → ( 𝐹 ∩ 𝐻 ) = ∅ )
18 15 17 eqtr3id ⊢ ( 𝜑 → ( 𝐻 ∩ 𝐹 ) = ∅ )
19 minel ⊢ ( ( 𝑌 ∈ 𝐹 ∧ ( 𝐻 ∩ 𝐹 ) = ∅ ) → ¬ 𝑌 ∈ 𝐻 )
20 9 18 19 syl2anc ⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝐻 )
21 difsnb ⊢ ( ¬ 𝑌 ∈ 𝐻 ↔ ( 𝐻 ∖ { 𝑌 } ) = 𝐻 )
22 20 21 sylib ⊢ ( 𝜑 → ( 𝐻 ∖ { 𝑌 } ) = 𝐻 )
23 22 uneq2d ⊢ ( 𝜑 → ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∖ { 𝑌 } ) ) = ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) )
24 14 23 eqtrid ⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) = ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) )
25 13 24 sseqtrrid ⊢ ( 𝜑 → 𝐻 ⊆ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) )
26 3 1 8 mrissd ⊢ ( 𝜑 → ( 𝐹 ∪ 𝐻 ) ⊆ 𝑋 )
27 26 ssdifssd ⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ⊆ 𝑋 )
28 1 2 27 mrcssidd ⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
29 25 28 sstrd ⊢ ( 𝜑 → 𝐻 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → 𝐻 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
31 12 30 unssd ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝐺 ∪ 𝐻 ) ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
32 11 2 mrcssvd ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ⊆ 𝑋 )
33 11 2 31 32 mrcssd ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ⊆ ( 𝑁 ‘ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) )
34 27 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ⊆ 𝑋 )
35 11 2 34 mrcidmd ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝑁 ‘ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) = ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
36 33 35 sseqtrd ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝑁 ‘ ( 𝐺 ∪ 𝐻 ) ) ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
37 10 36 sstrd ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → 𝐹 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
38 9 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → 𝑌 ∈ 𝐹 )
39 37 38 sseldd ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → 𝑌 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
40 8 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
41 ssun1 ⊢ 𝐹 ⊆ ( 𝐹 ∪ 𝐻 )
42 41 38 sselid ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → 𝑌 ∈ ( 𝐹 ∪ 𝐻 ) )
43 2 3 11 40 42 ismri2dad ⊢ ( ( 𝜑 ∧ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → ¬ 𝑌 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
44 39 43 pm2.65da ⊢ ( 𝜑 → ¬ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
45 nss ⊢ ( ¬ 𝐺 ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ↔ ∃ 𝑔 ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) )
46 44 45 sylib ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) )
47 simprl ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → 𝑔 ∈ 𝐺 )
48 ssun1 ⊢ ( 𝐹 ∖ { 𝑌 } ) ⊆ ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 )
49 48 24 sseqtrrid ⊢ ( 𝜑 → ( 𝐹 ∖ { 𝑌 } ) ⊆ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) )
50 49 28 sstrd ⊢ ( 𝜑 → ( 𝐹 ∖ { 𝑌 } ) ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( 𝐹 ∖ { 𝑌 } ) ⊆ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
52 simprr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) )
53 51 52 ssneldd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) )
54 unass ⊢ ( ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ∪ { 𝑔 } ) = ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) )
55 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
56 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ∀ 𝑠 ∈ 𝒫 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ ( ( 𝑁 ‘ ( 𝑠 ∪ { 𝑦 } ) ) ∖ ( 𝑁 ‘ 𝑠 ) ) 𝑦 ∈ ( 𝑁 ‘ ( 𝑠 ∪ { 𝑧 } ) ) )
57 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( 𝐹 ∪ 𝐻 ) ∈ 𝐼 )
58 difss ⊢ ( 𝐹 ∖ { 𝑌 } ) ⊆ 𝐹
59 unss1 ⊢ ( ( 𝐹 ∖ { 𝑌 } ) ⊆ 𝐹 → ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ⊆ ( 𝐹 ∪ 𝐻 ) )
60 58 59 mp1i ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ⊆ ( 𝐹 ∪ 𝐻 ) )
61 55 2 3 57 60 mrissmrid ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ∈ 𝐼 )
62 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → 𝐺 ⊆ ( 𝑋 ∖ 𝐻 ) )
63 62 difss2d ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → 𝐺 ⊆ 𝑋 )
64 63 47 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → 𝑔 ∈ 𝑋 )
65 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) = ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) )
66 65 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) = ( 𝑁 ‘ ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ) )
67 52 66 neleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ) )
68 55 2 3 56 61 64 67 mreexmrid ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( ( ( 𝐹 ∖ { 𝑌 } ) ∪ 𝐻 ) ∪ { 𝑔 } ) ∈ 𝐼 )
69 54 68 eqeltrrid ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 )
70 47 53 69 jca32 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) ) → ( 𝑔 ∈ 𝐺 ∧ ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) ) )
71 70 ex ⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → ( 𝑔 ∈ 𝐺 ∧ ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) ) ) )
72 71 eximdv ⊢ ( 𝜑 → ( ∃ 𝑔 ( 𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ ( 𝑁 ‘ ( ( 𝐹 ∪ 𝐻 ) ∖ { 𝑌 } ) ) ) → ∃ 𝑔 ( 𝑔 ∈ 𝐺 ∧ ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) ) ) )
73 46 72 mpd ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 ∈ 𝐺 ∧ ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) ) )
74 df-rex ⊢ ( ∃ 𝑔 ∈ 𝐺 ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) ↔ ∃ 𝑔 ( 𝑔 ∈ 𝐺 ∧ ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) ) )
75 73 74 sylibr ⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐺 ( ¬ 𝑔 ∈ ( 𝐹 ∖ { 𝑌 } ) ∧ ( ( 𝐹 ∖ { 𝑌 } ) ∪ ( 𝐻 ∪ { 𝑔 } ) ) ∈ 𝐼 ) )